merge master

doc/examples/bintree.lean

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros
+    split <;> (try simp) <;> split <;> (try simp)
     have_eq k k'
     contradiction
   | node left key value right ihl ihr =>

src/Init.lean

@@ -8,7 +8,6 @@ import Init.Prelude
 import Init.Notation
 import Init.Tactics
 import Init.TacticsExtra
-import Init.ByCases
 import Init.RCases
 import Init.Core
 import Init.Control
@@ -24,11 +23,8 @@ import Init.MetaTypes
 import Init.Meta
 import Init.NotationExtra
 import Init.SimpLemmas
-import Init.PropLemmas
 import Init.Hints
 import Init.Conv
 import Init.Guard
 import Init.Simproc
 import Init.SizeOfLemmas
-import Init.BinderPredicates
-import Init.Ext

src/Init/BinderPredicates.lean

@@ -1,82 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-prelude
-import Init.NotationExtra
-
-namespace Lean
-
-/--
-The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
-(`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
--/
-declare_syntax_cat binderPred
-
-/--
-`satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`.
--/
-syntax "satisfies_binder_pred% " term:max binderPred : term
-
--- Extend ∀ and ∃ to binder predicates.
-
-/--
-The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`,
-and similarly for other binary operators.
--/
-syntax "∃ " binderIdent binderPred ", " term : term
-/--
-The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`,
-and similarly for other binary operators.
--/
-syntax "∀ " binderIdent binderPred ", " term : term
-
-macro_rules
-  | `(∃ $x:ident $pred:binderPred, $p) =>
-    `(∃ $x:ident, satisfies_binder_pred% $x $pred ∧ $p)
-  | `(∃ _ $pred:binderPred, $p) =>
-    `(∃ x, satisfies_binder_pred% x $pred ∧ $p)
-
-macro_rules
-  | `(∀ $x:ident $pred:binderPred, $p) =>
-    `(∀ $x:ident, satisfies_binder_pred% $x $pred → $p)
-  | `(∀ _ $pred:binderPred, $p) =>
-    `(∀ x, satisfies_binder_pred% x $pred → $p)
-
-/-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...` -/
-binder_predicate x " > " y:term => `($x > $y)
-/-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...` -/
-binder_predicate x " ≥ " y:term => `($x ≥ $y)
-/-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...` -/
-binder_predicate x " < " y:term => `($x < $y)
-/-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...` -/
-binder_predicate x " ≤ " y:term => `($x ≤ $y)
-/-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
-binder_predicate x " ≠ " y:term => `($x ≠ $y)
-
-/-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for
-`∃ x, x ∈ y ∧ ...` -/
-binder_predicate x " ∈ " y:term => `($x ∈ $y)
-
-/-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for
-`∃ x, x ∉ y ∧ ...` -/
-binder_predicate x " ∉ " y:term => `($x ∉ $y)
-
-/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
-`∃ x, x ⊆ y ∧ ...` -/
-binder_predicate x " ⊆ " y:term => `($x ⊆ $y)
-
-/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
-`∃ x, x ⊂ y ∧ ...` -/
-binder_predicate x " ⊂ " y:term => `($x ⊂ $y)
-
-/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
-`∃ x, x ⊇ y ∧ ...` -/
-binder_predicate x " ⊇ " y:term => `($x ⊇ $y)
-
-/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
-`∃ x, x ⊃ y ∧ ...` -/
-binder_predicate x " ⊃ " y:term => `($x ⊃ $y)
-
-end Lean

src/Init/ByCases.lean

@@ -1,74 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
--/
-prelude
-import Init.Classical
-
-/-! # by_cases tactic and if-then-else support -/
-
-/--
-`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
--/
-syntax "by_cases " (atomic(ident " : "))? term : tactic
-
-macro_rules
-  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
-macro_rules
-  | `(tactic| by_cases $h : $e) =>
-    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)
-
-/-! ## if-then-else -/
-
-@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
-
-@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
-
-theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
-
-/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches. -/
-theorem apply_dite (f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) :
-    f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h)) := by
-  by_cases h : P <;> simp [h]
-
-/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches. -/
-theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
-    f (ite P x y) = ite P (f x) (f y) :=
-  apply_dite f P (fun _ => x) (fun _ => y)
-
-/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
-@[simp] theorem dite_not (P : Prop) {_ : Decidable P}  (x : ¬P → α) (y : ¬¬P → α) :
-    dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by
-  by_cases h : P <;> simp [h]
-
-/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
-@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x :=
-  dite_not P (fun _ => x) (fun _ => y)
-
-@[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
-    dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
-
-@[simp] theorem dite_eq_right_iff {P : Prop} [Decidable P] {A : P → α} :
-    (dite P A fun _ => b) = b ↔ ∀ h, A h = b := by
-  by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
-
-@[simp] theorem ite_eq_left_iff {P : Prop} [Decidable P] : ite P a b = a ↔ ¬P → b = a :=
-  dite_eq_left_iff
-
-@[simp] theorem ite_eq_right_iff {P : Prop} [Decidable P] : ite P a b = b ↔ P → a = b :=
-  dite_eq_right_iff
-
-/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
-@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
-
--- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
-theorem ite_some_none_eq_none [Decidable P] :
-    (if P then some x else none) = none ↔ ¬ P := by
-  simp only [ite_eq_right_iff]
-  rfl
-
-@[simp] theorem ite_some_none_eq_some [Decidable P] :
-    (if P then some x else none) = some y ↔ P ∧ x = y := by
-  split <;> simp_all

src/Init/Classical.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
-import Init.PropLemmas
+import Init.Core
+import Init.NotationExtra
 
 universe u v
 
@@ -111,8 +112,8 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (
 
 theorem propComplete (a : Prop) : a = True ∨ a = False :=
   match em a with
-  | Or.inl ha => Or.inl (eq_true ha)
-  | Or.inr hn => Or.inr (eq_false hn)
+  | Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
+  | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
 
 -- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
@@ -122,36 +123,15 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
-/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
-The left-to-right direction, double negation elimination (DNE),
-is classically true but not constructively. -/
-@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
-
-@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
-
-theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
-theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not
-
-theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
-  rw [← not_forall]; exact em _
-
-theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
-  rw [← not_exists]; exact em _
-
-theorem or_iff_not_imp_left  : a ∨ b ↔ (¬a → b) := Decidable.or_iff_not_imp_left
-theorem or_iff_not_imp_right : a ∨ b ↔ (¬b → a) := Decidable.or_iff_not_imp_right
-
-theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
-
-theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_or_not_not
-
-theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
-
 end Classical
 
-/-- Extract an element from a existential statement, using `Classical.choose`. -/
--- This enables projection notation.
-@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
+/--
+`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
+-/
+syntax "by_cases " (atomic(ident " : "))? term : tactic
 
-/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
-theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P
+macro_rules
+  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
+macro_rules
+  | `(tactic| by_cases $h : $e) =>
+    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)

src/Init/Control/Lawful.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
+Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
@@ -84,36 +84,6 @@ theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *>
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
   rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
 
-/--
-An alternative constructor for `LawfulMonad` which has more
-defaultable fields in the common case.
--/
-theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
-    (id_map : ∀ {α} (x : m α), id <$> x = x)
-    (pure_bind : ∀ {α β} (x : α) (f : α → m β), pure x >>= f = f x)
-    (bind_assoc : ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ),
-      x >>= f >>= g = x >>= fun x => f x >>= g)
-    (map_const : ∀ {α β} (x : α) (y : m β),
-      Functor.mapConst x y = Function.const β x <$> y := by intros; rfl)
-    (seqLeft_eq : ∀ {α β} (x : m α) (y : m β),
-      x <* y = (x >>= fun a => y >>= fun _ => pure a) := by intros; rfl)
-    (seqRight_eq : ∀ {α β} (x : m α) (y : m β), x *> y = (x >>= fun _ => y) := by intros; rfl)
-    (bind_pure_comp : ∀ {α β} (f : α → β) (x : m α),
-      x >>= (fun y => pure (f y)) = f <$> x := by intros; rfl)
-    (bind_map : ∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x := by intros; rfl)
-    : LawfulMonad m :=
-  have map_pure {α β} (g : α → β) (x : α) : g <$> (pure x : m α) = pure (g x) := by
-    rw [← bind_pure_comp]; simp [pure_bind]
-  { id_map, bind_pure_comp, bind_map, pure_bind, bind_assoc, map_pure,
-    comp_map := by simp [← bind_pure_comp, bind_assoc, pure_bind]
-    pure_seq := by intros; rw [← bind_map]; simp [pure_bind]
-    seq_pure := by intros; rw [← bind_map]; simp [map_pure, bind_pure_comp]
-    seq_assoc := by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind]
-    map_const := funext fun x => funext (map_const x)
-    seqLeft_eq := by simp [seqLeft_eq, ← bind_map, ← bind_pure_comp, pure_bind, bind_assoc]
-    seqRight_eq := fun x y => by
-      rw [seqRight_eq, ← bind_map, ← bind_pure_comp, bind_assoc]; simp [pure_bind, id_map] }
-
 /-! # Id -/
 
 namespace Id
@@ -203,16 +173,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 end ExceptT
 
-/-! # Except -/
-
-instance : LawfulMonad (Except ε) := LawfulMonad.mk'
-  (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun a f => rfl)
-  (bind_assoc := fun a f g => by cases a <;> rfl)
-
-instance : LawfulApplicative (Except ε) := inferInstance
-instance : LawfulFunctor (Except ε) := inferInstance
-
 /-! # ReaderT -/
 
 namespace ReaderT
@@ -347,30 +307,3 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   bind_assoc     := by intros; apply ext; intros; simp
 
 end StateT
-
-/-! # EStateM -/
-
-instance : LawfulMonad (EStateM ε σ) := .mk'
-  (id_map := fun x => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.map]
-    match x s with
-    | .ok _ _ => rfl
-    | .error _ _ => rfl)
-  (pure_bind := fun _ _ => rfl)
-  (bind_assoc := fun x _ _ => funext <| fun s => by
-    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
-    match x s with
-    | .ok _ _ => rfl
-    | .error _ _ => rfl)
-  (map_const := fun _ _ => rfl)
-
-/-! # Option -/
-
-instance : LawfulMonad Option := LawfulMonad.mk'
-  (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun x f => rfl)
-  (bind_assoc := fun x f g => by cases x <;> rfl)
-  (bind_pure_comp := fun f x => by cases x <;> rfl)
-
-instance : LawfulApplicative Option := inferInstance
-instance : LawfulFunctor Option := inferInstance

src/Init/Core.lean

@@ -17,9 +17,7 @@ universe u v w
 at the application site itself (by comparison to the `@[inline]` attribute,
 which applies to all applications of the function).
 -/
-@[simp] def inline {α : Sort u} (a : α) : α := a
-
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+def inline {α : Sort u} (a : α) : α := a
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -34,32 +32,8 @@ and `flip (·<·)` is the greater-than relation.
 
 @[simp] theorem Function.comp_apply {f : β → δ} {g : α → β} {x : α} : comp f g x = f (g x) := rfl
 
-theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g = fun x => f (g x) := rfl
-
 attribute [simp] namedPattern
 
-/--
-`Empty.elim : Empty → C` says that a value of any type can be constructed from
-`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
-
-This is a non-dependent variant of `Empty.rec`.
--/
-@[macro_inline] def Empty.elim {C : Sort u} : Empty → C := Empty.rec
-
-/-- Decidable equality for Empty -/
-instance : DecidableEq Empty := fun a => a.elim
-
-/--
-`PEmpty.elim : Empty → C` says that a value of any type can be constructed from
-`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
-
-This is a non-dependent variant of `PEmpty.rec`.
--/
-@[macro_inline] def PEmpty.elim {C : Sort _} : PEmpty → C := fun a => nomatch a
-
-/-- Decidable equality for PEmpty -/
-instance : DecidableEq PEmpty := fun a => a.elim
-
 /--
   Thunks are "lazy" values that are evaluated when first accessed using `Thunk.get/map/bind`.
   The value is then stored and not recomputed for all further accesses. -/
@@ -104,8 +78,6 @@ instance thunkCoe : CoeTail α (Thunk α) where
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h
 
-/-! # definitions  -/
-
 /--
 If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
 By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
@@ -154,10 +126,6 @@ inductive PSum (α : Sort u) (β : Sort v) where
 
 @[inherit_doc] infixr:30 " ⊕' " => PSum
 
-instance {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩
-
-instance {α β} [Inhabited β] : Inhabited (PSum α β) := ⟨PSum.inr default⟩
-
 /--
 `Sigma β`, also denoted `Σ a : α, β a` or `(a : α) × β a`, is the type of dependent pairs
 whose first component is `a : α` and whose second component is `b : β a`
@@ -374,70 +342,6 @@ class HasEquiv (α : Sort u) where
 
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
-/-! # set notation  -/
-
-/-- Notation type class for the subset relation `⊆`. -/
-class HasSubset (α : Type u) where
-  /-- Subset relation: `a ⊆ b`  -/
-  Subset : α → α → Prop
-export HasSubset (Subset)
-
-/-- Notation type class for the strict subset relation `⊂`. -/
-class HasSSubset (α : Type u) where
-  /-- Strict subset relation: `a ⊂ b`  -/
-  SSubset : α → α → Prop
-export HasSSubset (SSubset)
-
-/-- Superset relation: `a ⊇ b`  -/
-abbrev Superset [HasSubset α] (a b : α) := Subset b a
-
-/-- Strict superset relation: `a ⊃ b`  -/
-abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
-
-/-- Notation type class for the union operation `∪`. -/
-class Union (α : Type u) where
-  /-- `a ∪ b` is the union of`a` and `b`. -/
-  union : α → α → α
-
-/-- Notation type class for the intersection operation `∩`. -/
-class Inter (α : Type u) where
-  /-- `a ∩ b` is the intersection of`a` and `b`. -/
-  inter : α → α → α
-
-/-- Notation type class for the set difference `\`. -/
-class SDiff (α : Type u) where
-  /--
-  `a \ b` is the set difference of `a` and `b`,
-  consisting of all elements in `a` that are not in `b`.
-  -/
-  sdiff : α → α → α
-
-/-- Subset relation: `a ⊆ b`  -/
-infix:50 " ⊆ " => Subset
-
-/-- Strict subset relation: `a ⊂ b`  -/
-infix:50 " ⊂ " => SSubset
-
-/-- Superset relation: `a ⊇ b`  -/
-infix:50 " ⊇ " => Superset
-
-/-- Strict superset relation: `a ⊃ b`  -/
-infix:50 " ⊃ " => SSuperset
-
-/-- `a ∪ b` is the union of`a` and `b`. -/
-infixl:65 " ∪ " => Union.union
-
-/-- `a ∩ b` is the intersection of`a` and `b`. -/
-infixl:70 " ∩ " => Inter.inter
-
-/--
-`a \ b` is the set difference of `a` and `b`,
-consisting of all elements in `a` that are not in `b`.
--/
-infix:70 " \\ " => SDiff.sdiff
-
-/-! # collections  -/
-
 /-- `EmptyCollection α` is the typeclass which supports the notation `∅`, also written as `{}`. -/
 class EmptyCollection (α : Type u) where
   /-- `∅` or `{}` is the empty set or empty collection.
@@ -447,36 +351,6 @@ class EmptyCollection (α : Type u) where
 @[inherit_doc] notation "{" "}" => EmptyCollection.emptyCollection
 @[inherit_doc] notation "∅"     => EmptyCollection.emptyCollection
 
-/--
-Type class for the `insert` operation.
-Used to implement the `{ a, b, c }` syntax.
--/
-class Insert (α : outParam <| Type u) (γ : Type v) where
-  /-- `insert x xs` inserts the element `x` into the collection `xs`. -/
-  insert : α → γ → γ
-export Insert (insert)
-
-/--
-Type class for the `singleton` operation.
-Used to implement the `{ a, b, c }` syntax.
--/
-class Singleton (α : outParam <| Type u) (β : Type v) where
-  /-- `singleton x` is a collection with the single element `x` (notation: `{x}`). -/
-  singleton : α → β
-export Singleton (singleton)
-
-/-- `insert x ∅ = {x}` -/
-class IsLawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :
-    Prop where
-  /-- `insert x ∅ = {x}` -/
-  insert_emptyc_eq (x : α) : (insert x ∅ : β) = singleton x
-export IsLawfulSingleton (insert_emptyc_eq)
-
-/-- Type class used to implement the notation `{ a ∈ c | p a }` -/
-class Sep (α : outParam <| Type u) (γ : Type v) where
-  /-- Computes `{ a ∈ c | p a }`. -/
-  sep : (α → Prop) → γ → γ
-
 /--
 `Task α` is a primitive for asynchronous computation.
 It represents a computation that will resolve to a value of type `α`,
@@ -651,7 +525,9 @@ theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p :=
   fun hn : ¬ p => hn h
 
 -- proof irrelevance is built in
-theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
+theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
+
+theorem id.def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced
@@ -699,9 +575,8 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h
 
 theorem Ne.irrefl (h : a ≠ a) : False := h rfl
 
-theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm)
-
-theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
+theorem Ne.symm (h : a ≠ b) : b ≠ a :=
+  fun h₁ => h (h₁.symm)
 
 theorem false_of_ne : a ≠ a → False := Ne.irrefl
 
@@ -713,8 +588,8 @@ theorem ne_true_of_not : ¬p → p ≠ True :=
     have : ¬True := h ▸ hnp
     this trivial
 
-theorem true_ne_false : ¬True = False := ne_false_of_self trivial
-theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
+theorem true_ne_false : ¬True = False :=
+  ne_false_of_self trivial
 
 end Ne
 
@@ -793,29 +668,22 @@ protected theorem Iff.rfl {a : Prop} : a ↔ a :=
 
 macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
 
-theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
-
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
-  Iff.intro (h₂.mp ∘ h₁.mp) (h₁.mpr ∘ h₂.mpr)
+  Iff.intro
+    (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
+    (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
 
--- This is needed for `calc` to work with `iff`.
-instance : Trans Iff Iff Iff where
-  trans := Iff.trans
+theorem Iff.symm (h : a ↔ b) : b ↔ a :=
+  Iff.intro (Iff.mpr h) (Iff.mp h)
 
-theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
-theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
+theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
+  Iff.intro Iff.symm Iff.symm
 
-theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
-theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
-theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
+theorem Iff.of_eq (h : a = b) : a ↔ b :=
+  h ▸ Iff.refl _
 
-theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
-theorem And.comm : a ∧ b ↔ b ∧ a := Iff.intro And.symm And.symm
-theorem and_comm : a ∧ b ↔ b ∧ a := And.comm
-
-theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl
-theorem Or.comm : a ∨ b ↔ b ∨ a := Iff.intro Or.symm Or.symm
-theorem or_comm : a ∨ b ↔ b ∨ a := Or.comm
+theorem And.comm : a ∧ b ↔ b ∧ a := by
+  constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
 
 /-! # Exists -/
 
@@ -1015,13 +883,8 @@ protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (
   apply heq_of_eq
   apply Subsingleton.elim
 
-instance (p : Prop) : Subsingleton p := ⟨fun a b => proof_irrel a b⟩
-
-instance : Subsingleton Empty  := ⟨(·.elim)⟩
-instance : Subsingleton PEmpty := ⟨(·.elim)⟩
-
-instance [Subsingleton α] [Subsingleton β] : Subsingleton (α × β) :=
-  ⟨fun {..} {..} => by congr <;> apply Subsingleton.elim⟩
+instance (p : Prop) : Subsingleton p :=
+  ⟨fun a b => proofIrrel a b⟩
 
 instance (p : Prop) : Subsingleton (Decidable p) :=
   Subsingleton.intro fun
@@ -1032,9 +895,6 @@ instance (p : Prop) : Subsingleton (Decidable p) :=
       | isTrue t₂  => absurd t₂ f₁
       | isFalse _  => rfl
 
-example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
-  ⟨fun ⟨x, _⟩ ⟨y, _⟩ => by congr; exact Subsingleton.elim x y⟩
-
 theorem recSubsingleton
      {p : Prop} [h : Decidable p]
      {h₁ : p → Sort u}
@@ -1314,117 +1174,12 @@ gen_injective_theorems% Lean.Syntax
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
   ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 
-/-! # Prop lemmas -/
-
-/-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with
-the arguments flipped, but it is in the `Not` namespace so that projection notation can be used. -/
-def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
-
-/-- Non-dependent eliminator for `And`. -/
-abbrev And.elim (f : a → b → α) (h : a ∧ b) : α := f h.left h.right
-
-/-- Non-dependent eliminator for `Iff`. -/
-def Iff.elim (f : (a → b) → (b → a) → α) (h : a ↔ b) : α := f h.mp h.mpr
+/-! # Quotients -/
 
 /-- Iff can now be used to do substitutions in a calculation -/
 theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
   Eq.subst (propext h₁) h₂
 
-theorem Not.intro {a : Prop} (h : a → False) : ¬a := h
-
-theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a := mt H1 H2
-
-theorem not_congr (h : a ↔ b) : ¬a ↔ ¬b := ⟨mt h.2, mt h.1⟩
-
-theorem not_not_not : ¬¬¬a ↔ ¬a := ⟨mt not_not_intro, not_not_intro⟩
-
-theorem iff_of_true (ha : a) (hb : b) : a ↔ b := Iff.intro (fun _ => hb) (fun _ => ha)
-theorem iff_of_false (ha : ¬a) (hb : ¬b) : a ↔ b := Iff.intro ha.elim hb.elim
-
-theorem iff_true_left  (ha : a) : (a ↔ b) ↔ b := Iff.intro (·.mp ha) (iff_of_true ha)
-theorem iff_true_right (ha : a) : (b ↔ a) ↔ b := Iff.comm.trans (iff_true_left ha)
-
-theorem iff_false_left  (ha : ¬a) : (a ↔ b) ↔ ¬b := Iff.intro (mt ·.mpr ha) (iff_of_false ha)
-theorem iff_false_right (ha : ¬a) : (b ↔ a) ↔ ¬b := Iff.comm.trans (iff_false_left ha)
-
-theorem of_iff_true    (h : a ↔ True) : a := h.mpr trivial
-theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h trivial
-
-theorem not_of_iff_false : (p ↔ False) → ¬p := Iff.mp
-theorem iff_false_intro (h : ¬a) : a ↔ False := iff_of_false h id
-
-theorem not_iff_false_intro (h : a) : ¬a ↔ False := iff_false_intro (not_not_intro h)
-theorem not_true : (¬True) ↔ False := iff_false_intro (not_not_intro trivial)
-
-theorem not_false_iff : (¬False) ↔ True := iff_true_intro not_false
-
-theorem Eq.to_iff : a = b → (a ↔ b) := Iff.of_eq
-theorem iff_of_eq : a = b → (a ↔ b) := Iff.of_eq
-theorem neq_of_not_iff : ¬(a ↔ b) → a ≠ b := mt Iff.of_eq
-
-theorem iff_iff_eq : (a ↔ b) ↔ a = b := Iff.intro propext Iff.of_eq
-@[simp] theorem eq_iff_iff : (a = b) ↔ (a ↔ b) := iff_iff_eq.symm
-
-theorem eq_self_iff_true (a : α)  : a = a ↔ True  := iff_true_intro rfl
-theorem ne_self_iff_false (a : α) : a ≠ a ↔ False := not_iff_false_intro rfl
-
-theorem false_of_true_iff_false (h : True ↔ False) : False := h.mp trivial
-theorem false_of_true_eq_false  (h : True = False) : False := false_of_true_iff_false (Iff.of_eq h)
-
-theorem true_eq_false_of_false : False → (True = False) := False.elim
-
-theorem iff_def  : (a ↔ b) ↔ (a → b) ∧ (b → a) := iff_iff_implies_and_implies a b
-theorem iff_def' : (a ↔ b) ↔ (b → a) ∧ (a → b) := Iff.trans iff_def And.comm
-
-theorem true_iff_false : (True ↔ False) ↔ False := iff_false_intro (·.mp  True.intro)
-theorem false_iff_true : (False ↔ True) ↔ False := iff_false_intro (·.mpr True.intro)
-
-theorem iff_not_self : ¬(a ↔ ¬a) | H => let f h := H.1 h h; f (H.2 f)
-theorem heq_self_iff_true (a : α) : HEq a a ↔ True := iff_true_intro HEq.rfl
-
-/-! ## implies -/
-
-theorem not_not_of_not_imp : ¬(a → b) → ¬¬a := mt Not.elim
-
-theorem not_of_not_imp {a : Prop} : ¬(a → b) → ¬b := mt fun h _ => h
-
-@[simp] theorem imp_not_self : (a → ¬a) ↔ ¬a := Iff.intro (fun h ha => h ha ha) (fun h _ => h)
-
-theorem imp_intro {α β : Prop} (h : α) : β → α := fun _ => h
-
-theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) := (h₁ ∘ · ∘ h₀)
-
-theorem imp_iff_right {a : Prop} (ha : a) : (a → b) ↔ b := Iff.intro (· ha) (fun a _ => a)
-
--- This is not marked `@[simp]` because we have `implies_true : (α → True) = True`
-theorem imp_true_iff (α : Sort u) : (α → True) ↔ True := iff_true_intro (fun _ => trivial)
-
-theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro False.elim
-
-theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro
-
-@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
-
-theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
-
-theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
-
-theorem imp_not_comm : (a → ¬b) ↔ (b → ¬a) := imp.swap
-
-theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := Iff.intro (· ∘ h.mpr) (· ∘ h.mp)
-
-theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
-  Iff.intro (fun hab ha => (h ha).mp (hab ha)) (fun hcd ha => (h ha).mpr (hcd ha))
-
-theorem imp_congr_ctx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
-  Iff.trans (imp_congr_left h₁) (imp_congr_right h₂)
-
-theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := imp_congr_ctx h₁ fun _ => h₂
-
-theorem imp_iff_not (hb : ¬b) : a → b ↔ ¬a := imp_congr_right fun _ => iff_false_intro hb
-
-/-! # Quotients -/
-
 namespace Quot
 /--
 The **quotient axiom**, or at least the nontrivial part of the quotient

src/Init/Data/Array/DecidableEq.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
-import Init.ByCases
+import Init.Classical
 
 namespace Array
 

src/Init/Data/Fin/Basic.lean

@@ -106,8 +106,6 @@ instance instOfNat : OfNat (Fin (no_index (n+1))) i where
 instance : Inhabited (Fin (no_index (n+1))) where
   default := 0
 
-@[simp] theorem zero_eta : (⟨0, Nat.zero_lt_succ _⟩ : Fin (n + 1)) = 0 := rfl
-
 theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
   fun h' => absurd (eq_of_val_eq h') h
 

src/Init/Data/List/Basic.lean

@@ -603,27 +603,6 @@ The longer list is truncated to match the shorter list.
 def zip : List α → List β → List (Prod α β) :=
   zipWith Prod.mk
 
-/--
-`O(max |xs| |ys|)`.
-Version of `List.zipWith` that continues to the end of both lists,
-passing `none` to one argument once the shorter list has run out.
--/
-def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
-  | [], bs => bs.map fun b => f none (some b)
-  | a :: as, [] => (a :: as).map fun a => f (some a) none
-  | a :: as, b :: bs => f a b :: zipWithAll f as bs
-
-@[simp] theorem zipWithAll_nil_right :
-    zipWithAll f as [] = as.map fun a => f (some a) none := by
-  cases as <;> rfl
-
-@[simp] theorem zipWithAll_nil_left :
-    zipWithAll f [] bs = bs.map fun b => f none (some b) := by
-  rfl
-
-@[simp] theorem zipWithAll_cons_cons :
-    zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: zipWithAll f as bs := rfl
-
 /--
 `O(|l|)`. Separates a list of pairs into two lists containing the first components and second components.
 * `unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])`
@@ -897,7 +876,7 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
       cases bs with
       | nil => intro h; contradiction
       | cons b bs =>
-        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl, -and_imp]
+        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl]
         intro ⟨h₁, h₂⟩
         exact ⟨h₁, ih h₂⟩
   rfl {as} := by

src/Init/Data/Nat.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
-import Init.Data.Nat.Dvd
 import Init.Data.Nat.Gcd
-import Init.Data.Nat.MinMax
 import Init.Data.Nat.Bitwise
 import Init.Data.Nat.Control
 import Init.Data.Nat.Log2

src/Init/Data/Nat/Basic.lean

@@ -147,20 +147,13 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by
 
 protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by
   induction n with
-  | zero => simp
+  | zero => simp; intros; assumption
   | succ n ih => simp [succ_add]; intro h; apply ih h
 
 protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
   apply Nat.add_left_cancel h
 
-theorem eq_zero_of_add_eq_zero : ∀ {n m}, n + m = 0 → n = 0 ∧ m = 0
-  | 0, 0, _ => ⟨rfl, rfl⟩
-  | _+1, 0, h => Nat.noConfusion h
-
-protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 :=
-  (Nat.eq_zero_of_add_eq_zero h).2
-
 /-! # Nat.mul theorems -/
 
 @[simp] protected theorem mul_zero (n : Nat) : n * 0 = 0 :=
@@ -213,13 +206,16 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
 
 attribute [simp] Nat.le_refl
 
-theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
+theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
+  succ_le_succ
 
-theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
+theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m :=
+  succ_le_succ
 
-@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
+@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n :=
+  rfl
 
-@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -245,7 +241,8 @@ theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
       show n - m < succ n from
       lt_succ_of_le (sub_le n m)
 
-theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
+theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) :=
+  rfl
 
 theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
   succ_sub_succ_eq_sub n m
@@ -280,24 +277,20 @@ instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop)
 protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m :=
   p ▸ Nat.le_refl n
 
+theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m :=
+  Nat.le_trans (le_succ n) h
+
+protected theorem le_of_lt {n m : Nat} (h : n < m) : n ≤ m :=
+  le_of_succ_le h
+
 theorem lt.step {n m : Nat} : n < m → n < succ m := le_step
 
-theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := Nat.le_trans (le_succ n) h
-theorem lt_of_succ_lt      {n m : Nat} : succ n < m → n < m := le_of_succ_le
-protected theorem le_of_lt {n m : Nat} : n < m → n ≤ m := le_of_succ_le
-
-theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := le_of_succ_le_succ
-
-theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := h
-theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := h
-
 theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
   | 0   => Or.inl rfl
   | _+1 => Or.inr (succ_pos _)
 
-protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
-
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
+
 theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
@@ -305,7 +298,20 @@ protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   | Or.inl h => Or.inl (Nat.le_of_lt h)
   | Or.inr h => Or.inr h
 
-theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 := Nat.le_antisymm h (zero_le _)
+theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 :=
+  Nat.le_antisymm h (zero_le _)
+
+theorem lt_of_succ_lt {n m : Nat} : succ n < m → n < m :=
+  le_of_succ_le
+
+theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m :=
+  le_of_succ_le_succ
+
+theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m :=
+  h
+
+theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m :=
+  h
 
 theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
   | 0,   _, h => h
@@ -320,7 +326,8 @@ theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by
 
 attribute [simp] Nat.lt_irrefl
 
-theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b := fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
+theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
+  fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
 
 theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :=
   Decidable.byCases
@@ -356,51 +363,16 @@ protected theorem not_le_of_gt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁
   | Or.inr h₂ =>
     have Heq : n = m := Nat.le_antisymm h₁ h₂
     absurd (@Eq.subst _ _ _ _ Heq h) (Nat.lt_irrefl m)
-protected theorem not_le_of_lt : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
-protected theorem not_lt_of_ge : ∀{a b : Nat}, b ≥ a → ¬(b < a) := flip Nat.not_le_of_gt
-protected theorem not_lt_of_le : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
-protected theorem lt_le_asymm : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
-protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
 
-theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
-protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
-protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
+theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m :=
+  match Nat.lt_or_ge m n with
+  | Or.inl h₁ => h₁
+  | Or.inr h₁ => absurd h₁ h
 
-theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
-protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
-protected theorem le_of_not_lt : ∀{a b : Nat}, ¬(a < b) → b ≤ a := Nat.ge_of_not_lt
-
-theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm
-protected theorem ne_of_lt' : ∀{a b : Nat}, a < b → b ≠ a := ne_of_gt
-
-@[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a :=
-  Iff.intro Nat.gt_of_not_le Nat.not_le_of_gt
-@[simp] protected theorem not_lt {a b : Nat} : ¬ a < b ↔ b ≤ a :=
-  Iff.intro Nat.ge_of_not_lt (flip Nat.not_le_of_gt)
-
-protected theorem le_of_not_le {a b : Nat} (h : ¬ b ≤ a) : a ≤ b := Nat.le_of_lt (Nat.not_le.1 h)
-protected theorem le_of_not_ge : ∀{a b : Nat}, ¬(a ≥ b) → a ≤ b:= @Nat.le_of_not_le
-
-protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a :=
-  match Nat.lt_or_ge a b with
-  | .inl h => .inl h
-  | .inr h =>
-    match Nat.eq_or_lt_of_le h with
-    | .inl h => .inr (.inl h.symm)
-    | .inr h => .inr (.inr h)
-
-protected theorem lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) : a < b ∨ a > b :=
-  match Nat.lt_trichotomy a b with
-  | .inl h => .inl h
-  | .inr (.inl e) => False.elim (ne e)
-  | .inr (.inr h) => .inr h
-
-protected theorem lt_or_lt_of_ne : ∀{a b : Nat}, a ≠ b → a < b ∨ b < a := Nat.lt_or_gt_of_ne
-
-protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
-  Iff.intro (fun p => And.intro (Nat.le_of_eq p) (Nat.le_of_eq p.symm))
-            (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
-protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
+theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m :=
+  match Nat.lt_or_ge n m with
+  | Or.inl h₁ => absurd h₁ h
+  | Or.inr h₁ => h₁
 
 instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
@@ -429,8 +401,6 @@ protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m
 protected theorem zero_lt_one : 0 < (1:Nat) :=
   zero_lt_succ 0
 
-protected theorem pos_iff_ne_zero : 0 < n ↔ n ≠ 0 := ⟨ne_of_gt, Nat.pos_of_ne_zero⟩
-
 theorem add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
   Nat.le_trans (Nat.add_le_add_right h₁ c) (Nat.add_le_add_left h₂ b)
 
@@ -448,9 +418,6 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a
   rw [Nat.add_comm _ b, Nat.add_comm _ b]
   apply Nat.le_of_add_le_add_left
 
-protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k :=
-  ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩
-
 /-! # Basic theorems for comparing numerals -/
 
 theorem ctor_eq_zero : Nat.zero = 0 :=
@@ -560,20 +527,7 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
 theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
-/-! # pred theorems -/
-
-@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
-@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
-
-theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
-  induction a with
-  | zero => contradiction
-  | succ => rfl
-
-theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n
-  | _+1, _ => rfl
-
-/-! # sub theorems -/
+/-! # sub/pred theorems -/
 
 theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
   induction a with
@@ -607,6 +561,11 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
   apply Nat.zero_lt_sub_of_lt
   assumption
 
+theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
+  induction a with
+  | zero => contradiction
+  | succ => rfl
+
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
   | 0, succ b, _ => by simp
@@ -632,7 +591,7 @@ protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m :=
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
 
-@[simp] protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
+protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
   suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
   by rw [Nat.add_sub_add_right, Nat.sub_zero]
 
@@ -721,6 +680,12 @@ theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b :=
   have : a.succ + b ≤ c := by simp [Nat.succ_add]; exact h
   le_sub_of_add_le this
 
+@[simp] protected theorem pred_zero : pred 0 = 0 :=
+  rfl
+
+@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n :=
+  rfl
+
 theorem sub.elim {motive : Nat → Prop}
     (x y : Nat)
     (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k)
@@ -730,75 +695,18 @@ theorem sub.elim {motive : Nat → Prop}
   | inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt
   | inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm
 
-theorem succ_sub {m n : Nat} (h : n ≤ m) : succ m - n = succ (m - n) := by
-  let ⟨k, hk⟩ := Nat.le.dest h
-  rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left]
-
-protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m :=
-  Nat.pos_iff_ne_zero.2 (Nat.sub_ne_zero_of_lt h)
-
-protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
-  induction k with
-  | zero => simp
-  | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
-
-protected theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n :=
-  match m, le.dest h with
-  | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le
-
-protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤ m - k
-  | 0   => h
-  | z+1 => pred_le_pred (Nat.sub_le_sub_right h z)
-
-protected theorem lt_of_sub_ne_zero (h : n - m ≠ 0) : m < n :=
-  Nat.not_le.1 (mt Nat.sub_eq_zero_of_le h)
-
-protected theorem sub_ne_zero_iff_lt : n - m ≠ 0 ↔ m < n :=
-  ⟨Nat.lt_of_sub_ne_zero, Nat.sub_ne_zero_of_lt⟩
-
-protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n :=
-  Nat.lt_of_sub_ne_zero (Nat.pos_iff_ne_zero.1 h)
-
-protected theorem lt_of_sub_eq_succ (h : m - n = succ l) : n < m :=
-  Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _)
-
-protected theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by
-  have := Nat.sub_le_sub_right (succ_le_of_lt h) n
-  rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this
-
-protected theorem sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) : k - n < m :=
-  Nat.sub_lt_left_of_lt_add H (Nat.add_comm .. ▸ h)
-
-protected theorem le_of_sub_eq_zero : ∀ {n m}, n - m = 0 → n ≤ m
-  | 0, _, _ => Nat.zero_le ..
-  | _+1, _+1, h => Nat.succ_le_succ <| Nat.le_of_sub_eq_zero (Nat.succ_sub_succ .. ▸ h)
-
-protected theorem le_of_sub_le_sub_right : ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m
-  | 0, _, _, _, _ => Nat.zero_le ..
-  | _+1, _, 0, _, h₁ => h₁
-  | _+1, _+1, _+1, h₀, h₁ => by
-    simp only [Nat.succ_sub_succ] at h₁
-    exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁
-
-protected theorem sub_le_sub_iff_right {n : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
-  ⟨Nat.le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h _⟩
-
-protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = c + b :=
-  ⟨fun | rfl => by rw [Nat.sub_add_cancel h], fun heq => by rw [heq, Nat.add_sub_cancel]⟩
-
-protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
-  rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
-
 theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
   cases n with
   | zero   => simp
   | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
 
-/-! ## Mul sub distrib -/
-
 theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
   rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
 
+protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
+  induction k with
+  | zero => simp
+  | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
 
 protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k := by
   induction m with
@@ -811,12 +719,14 @@ protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n *
 /-! # Helper normalization theorems -/
 
 theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) :=
-  Eq.propIntro Nat.gt_of_not_le Nat.not_le_of_gt
+  propext <| Iff.intro (fun h => Nat.gt_of_not_le h) (fun h => Nat.not_le_of_gt h)
+
 theorem not_ge_eq (a b : Nat) : (¬ (a ≥ b)) = (a + 1 ≤ b) :=
   not_le_eq b a
 
 theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) :=
-  Eq.propIntro Nat.le_of_not_lt Nat.not_lt_of_le
+  propext <| Iff.intro (fun h => have h := Nat.succ_le_of_lt (Nat.gt_of_not_le h); Nat.le_of_succ_le_succ h) (fun h => Nat.not_le_of_gt (Nat.succ_le_succ h))
+
 theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   not_lt_eq b a
 

src/Init/Data/Nat/Div.lean

@@ -7,7 +7,6 @@ prelude
 import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
-
 namespace Nat
 
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
@@ -175,136 +174,4 @@ theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
     rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
 decreasing_by apply div_rec_lemma; assumption
 
-theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by
- rw [div_eq a, if_pos]; constructor <;> assumption
-
-
-theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
-  induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
-  | base x y h => simp [h]
-  | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
-
-@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by
-  have := mod_add_div n 1
-  rwa [mod_one, Nat.zero_add, Nat.one_mul] at this
-
-@[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by
-  rw [div_eq]; simp [Nat.lt_irrefl]
-
-@[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 :=
-  (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt
-
-theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
-  induction y, k using mod.inductionOn generalizing x with
-    (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
-  | base y k h =>
-    simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
-    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
-    exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
-  | ind y k h IH =>
-    rw [← add_one, Nat.add_le_add_iff_right, IH k0, succ_mul,
-        ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]
-
-theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
-  | m, 0   => by simp
-  | m, n+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)
-
-theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
-  rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
-
-@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
-  rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
-
-@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
-  rw [Nat.add_comm, add_div_right x H]
-
-theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
-  induction z with
-  | zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
-  | succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl
-
-theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y := by
-  rw [Nat.mul_comm, add_mul_div_left _ _ H]
-
-@[simp] theorem add_mod_right (x z : Nat) : (x + z) % z = x % z := by
-  rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel]
-
-@[simp] theorem add_mod_left (x z : Nat) : (x + z) % x = z % x := by
-  rw [Nat.add_comm, add_mod_right]
-
-@[simp] theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y := by
-  match z with
-  | 0 => rw [Nat.mul_zero, Nat.add_zero]
-  | succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]
-
-@[simp] theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z := by
-  rw [Nat.mul_comm, add_mul_mod_self_left]
-
-@[simp] theorem mul_mod_right (m n : Nat) : (m * n) % m = 0 := by
-  rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod]
-
-@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
-  rw [Nat.mul_comm, mul_mod_right]
-
-protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
-have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
-  rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
-Nat.le_antisymm
-  (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
-  ((Nat.le_div_iff_mul_le npos).2 lo)
-
-theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
-  match eq_zero_or_pos n with
-  | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
-  | .inr h₀ => induction p with
-    | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
-    | succ p IH =>
-      have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
-      have h₃ : x - n * p ≥ n := by
-        apply Nat.le_of_add_le_add_right
-        rw [Nat.sub_add_cancel h₂, Nat.add_comm]
-        rw [mul_succ] at h₁
-        exact h₁
-      rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
-      simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
-
-theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
-  have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
-    rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
-  apply Nat.div_eq_of_lt_le
-  focus
-    rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
-    exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _
-  focus
-    show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
-    rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
-      fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed?
-    focus
-      rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
-      exact Nat.sub_le_sub_left (div_mul_le_self ..) _
-    focus
-      rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]
-
-theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
-  if y0 : y = 0 then by
-    rw [y0, Nat.mul_zero, mod_zero, mod_zero]
-  else if z0 : z = 0 then by
-    rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
-  else by
-    induction x using Nat.strongInductionOn with
-    | _ n IH =>
-      have y0 : y > 0 := Nat.pos_of_ne_zero y0
-      have z0 : z > 0 := Nat.pos_of_ne_zero z0
-      cases Nat.lt_or_ge n y with
-      | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
-      | inr yn =>
-        rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
-          ← Nat.mul_sub_left_distrib]
-        exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)
-
-theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
-  rw [div_eq a, if_neg]
-  intro h₁
-  apply Nat.not_le_of_gt h₀ h₁.right
-
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -1,96 +0,0 @@
-prelude
-import Init.Data.Nat.Div
-
-namespace Nat
-
-/--
-Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
-there is some `c` such that `b = a * c`.
--/
-instance : Dvd Nat where
-  dvd a b := Exists (fun c => b = a * c)
-
-protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
-
-protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
-
-protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
-protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩
-
-protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
-  match h₁, h₂ with
-  | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
-    ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩
-
-protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
-  let ⟨c, H'⟩ := h; H'.trans c.zero_mul
-
-@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
-  ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩
-
-protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
-  let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩
-
-protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
-  ⟨Nat.dvd_add h,
-    match m, h with
-    | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ =>
-      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩
-
-protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
-  rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
-
-theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
-  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
-  by rwa [mod_add_div] at this
-
-theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
-  | ⟨k, e⟩ => by
-    revert h
-    rw [e]
-    match k with
-    | 0 => intro hn; simp at hn
-    | pk+1 =>
-      intro
-      have := Nat.mul_le_mul_left m (succ_pos pk)
-      rwa [Nat.mul_one] at this
-
-protected theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
-  | _, 0, _, h₂ => Nat.eq_zero_of_zero_dvd h₂
-  | 0, _, h₁, _ => (Nat.eq_zero_of_zero_dvd h₁).symm
-  | _+1, _+1, h₁, h₂ => Nat.le_antisymm (le_of_dvd (succ_pos _) h₁) (le_of_dvd (succ_pos _) h₂)
-
-theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m :=
-  Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1)
-
-@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
-
-theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd
-
-theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by
-  let ⟨z, H⟩ := H; rw [H, mul_mod_right]
-
-theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by
-  exists n / m
-  have := (mod_add_div n m).symm
-  rwa [H, Nat.zero_add] at this
-
-theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 :=
-  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
-
-instance decidable_dvd : @DecidableRel Nat (·∣·) :=
-  fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm
-
-theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
-  rw [dvd_iff_mod_eq_zero] at h
-  exact Nat.pos_of_ne_zero h
-
-
-protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by
-  have := mod_add_div m n
-  rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this
-
-protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
-  rw [Nat.mul_comm, Nat.mul_div_cancel' H]
-
-end Nat

src/Init/Data/Nat/Gcd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Nat.Dvd
+import Init.Data.Nat.Div
 
 namespace Nat
 
@@ -38,35 +38,4 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
 
-theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
-  match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
-  | _ + 1 => by simp [gcd_succ]
-
-@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
-    (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
-  Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
-    (fun
-    | 0, _ => H0
-    | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
-    n
-
-theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by
-  induction m, n using gcd.induction with
-  | H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
-  | H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩
-
-theorem gcd_dvd_left (m n : Nat) : gcd m n ∣ m := (gcd_dvd m n).left
-
-theorem gcd_dvd_right (m n : Nat) : gcd m n ∣ n := (gcd_dvd m n).right
-
-theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n
-
-theorem gcd_le_right (n) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n
-
-theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
-  induction m, n using gcd.induction with intro km kn
-  | H0 n => rw [gcd_zero_left]; exact kn
-  | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
-
 end Nat

src/Init/Data/Nat/Linear.lean

@@ -5,7 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Coe
-import Init.ByCases
+import Init.Classical
+import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.List.Basic
 import Init.Data.Prod
@@ -538,13 +539,13 @@ theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b
 theorem Expr.of_cancel_eq (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx = b.denote ctx) = (c.denote ctx = d.denote ctx) := by
   have := Poly.denote_eq_cancel_eq ctx a.toNormPoly b.toNormPoly
   rw [h] at this
-  simp [toNormPoly, Poly.norm, Poly.denote_eq, -eq_iff_iff] at this
+  simp [toNormPoly, Poly.norm, Poly.denote_eq] at this
   exact this.symm
 
 theorem Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx ≤ b.denote ctx) = (c.denote ctx ≤ d.denote ctx) := by
   have := Poly.denote_le_cancel_eq ctx a.toNormPoly b.toNormPoly
   rw [h] at this
-  simp [toNormPoly, Poly.norm,Poly.denote_le, -eq_iff_iff] at this
+  simp [toNormPoly, Poly.norm,Poly.denote_le] at this
   exact this.symm
 
 theorem Expr.of_cancel_lt (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.inc.toNormPoly b.toNormPoly = (c.inc.toPoly, d.toPoly)) : (a.denote ctx < b.denote ctx) = (c.denote ctx < d.denote ctx) :=
@@ -589,7 +590,7 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : (1 == (0 : Nat)) = false := rfl
   have : (1 == (1 : Nat)) = true  := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
-     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
+     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
   · rw [h]
   · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
@@ -636,18 +637,20 @@ theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) :
 theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
   cases c; rename_i eq lhs rhs
   simp [isUnsat]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro
       | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₂]
-    exact Poly.of_isNonZero ctx h₁
+    have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁)
+    simp [this]
+    done
 
 theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by
   cases c; rename_i eq lhs rhs
   simp [isValid]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
   · intro h
@@ -655,12 +658,12 @@ theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid
 
 theorem ExprCnstr.eq_false_of_isUnsat (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isUnsat) : c.denote ctx = False := by
   have := PolyCnstr.eq_false_of_isUnsat ctx h
-  simp [-eq_iff_iff] at this
+  simp at this
   assumption
 
 theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toNormPoly.isValid) : c.denote ctx = True := by
   have := PolyCnstr.eq_true_of_isValid ctx h
-  simp [-eq_iff_iff] at this
+  simp at this
   assumption
 
 theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certificate) (h : (combineHyps c cs).denote ctx → False) : c.denote ctx → cs.denote ctx := by
@@ -709,7 +712,7 @@ theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.
 
 theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by
   have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
-  simp [-eq_iff_iff] at h
+  simp at h
   assumption
 
 theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by

src/Init/Data/Nat/MinMax.lean

@@ -1,51 +0,0 @@
-prelude
-import Init.ByCases
-
-namespace Nat
-
-/-! # min lemmas -/
-
-protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl
-
-protected theorem min_comm (a b : Nat) : min a b = min b a := by
-  match Nat.lt_trichotomy a b with
-  | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
-  | .inr (.inl h) => simp [Nat.min_def, h]
-  | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
-
-protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
-  by_cases (a <= b) <;> simp [Nat.min_def, *]
-protected theorem min_le_left (a b : Nat) : min a b ≤ a :=
-  Nat.min_comm .. ▸ Nat.min_le_right ..
-
-protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
-protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
-  Nat.min_comm .. ▸ Nat.min_eq_left h
-
-protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
-  intros; cases Nat.le_total b c with
-  | inl h => rw [Nat.min_eq_left h]; assumption
-  | inr h => rw [Nat.min_eq_right h]; assumption
-
-protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
-  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
-   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
-
-protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min
-
-/-! # max lemmas -/
-
-protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl
-
-protected theorem max_comm (a b : Nat) : max a b = max b a := by
-  simp only [Nat.max_def]
-  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
-  · exact Nat.le_antisymm h₂ h₁
-  · cases not_or_intro h₁ h₂ <| Nat.le_total ..
-
-protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by
-  by_cases (a <= b) <;> simp [Nat.max_def, *]
-protected theorem le_max_right (a b : Nat) : b ≤ max a b :=
-   Nat.max_comm .. ▸ Nat.le_max_left ..
-
-end Nat

src/Init/Data/Nat/Power2.lean

@@ -8,8 +8,6 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
-protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
-
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]

src/Init/Ext.lean

@@ -1,113 +0,0 @@
-/-
-Copyright (c) 2021 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro
--/
-prelude
-import Init.TacticsExtra
-import Init.RCases
-
-namespace Lean
-namespace Parser.Attr
-/-- Registers an extensionality theorem.
-
-* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
-  them for the `ext` tactic.
-
-* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic.
-
-* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
-
-* The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
-  rather than flattening the parents' fields into the lemma's equality hypotheses.
-  structures in the generated extensionality theorems. -/
-syntax (name := ext) "ext" (" (" &"flat" " := " term ")")? (ppSpace prio)? : attr
-end Parser.Attr
-
--- TODO: rename this namespace?
--- Remark: `ext` has scoped syntax, Mathlib may depend on the actual namespace name.
-namespace Elab.Tactic.Ext
-/--
-Creates the type of the extensionality theorem for the given structure,
-elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
--/
-scoped syntax (name := extType) "ext_type% " term:max ppSpace ident : term
-
-/--
-Creates the type of the iff-variant of the extensionality theorem for the given structure,
-elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
--/
-scoped syntax (name := extIffType) "ext_iff_type% " term:max ppSpace ident : term
-
-/--
-`declare_ext_theorems_for A` declares the extensionality theorems for the structure `A`.
-
-These theorems state that two expressions with the structure type are equal if their fields are equal.
--/
-syntax (name := declareExtTheoremFor) "declare_ext_theorems_for " ("(" &"flat" " := " term ") ")? ident (ppSpace prio)? : command
-
-macro_rules | `(declare_ext_theorems_for $[(flat := $f)]? $struct:ident $(prio)?) => do
-  let flat := f.getD (mkIdent `true)
-  let names ← Macro.resolveGlobalName struct.getId.eraseMacroScopes
-  let name ← match names.filter (·.2.isEmpty) with
-    | [] => Macro.throwError s!"unknown constant {struct.getId}"
-    | [(name, _)] => pure name
-    | _ => Macro.throwError s!"ambiguous name {struct.getId}"
-  let extName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext"
-  let extIffName := mkIdentFrom struct (canonical := true) <| name.mkStr "ext_iff"
-  `(@[ext $(prio)?] protected theorem $extName:ident : ext_type% $flat $struct:ident :=
-      fun {..} {..} => by intros; subst_eqs; rfl
-    protected theorem $extIffName:ident : ext_iff_type% $flat $struct:ident :=
-      fun {..} {..} =>
-        ⟨fun h => by cases h; and_intros <;> rfl,
-         fun _ => by (repeat cases ‹_ ∧ _›); subst_eqs; rfl⟩)
-
-/--
-Applies extensionality lemmas that are registered with the `@[ext]` attribute.
-* `ext pat*` applies extensionality theorems as much as possible,
-  using the patterns `pat*` to introduce the variables in extensionality theorems using `rintro`.
-  For example, the patterns are used to name the variables introduced by lemmas such as `funext`.
-* Without patterns,`ext` applies extensionality lemmas as much
-  as possible but introduces anonymous hypotheses whenever needed.
-* `ext pat* : n` applies ext theorems only up to depth `n`.
-
-The `ext1 pat*` tactic is like `ext pat*` except that it only applies a single extensionality theorem.
-
-Unused patterns will generate warning.
-Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.
--/
-syntax (name := ext) "ext" (colGt ppSpace rintroPat)* (" : " num)? : tactic
-
-/-- Apply a single extensionality theorem to the current goal. -/
-syntax (name := applyExtTheorem) "apply_ext_theorem" : tactic
-
-/--
-`ext1 pat*` is like `ext pat*` except that it only applies a single extensionality theorem rather
-than recursively applying as many extensionality theorems as possible.
-
-The `pat*` patterns are processed using the `rintro` tactic.
-If no patterns are supplied, then variables are introduced anonymously using the `intros` tactic.
--/
-macro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
-  if xs.isEmpty then `(tactic| apply_ext_theorem <;> intros)
-  else `(tactic| apply_ext_theorem <;> rintro $xs*)
-
-end Elab.Tactic.Ext
-end Lean
-
-attribute [ext] funext propext Subtype.eq
-
-@[ext] theorem Prod.ext : {x y : Prod α β} → x.fst = y.fst → x.snd = y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
-
-@[ext] theorem PProd.ext : {x y : PProd α β} → x.fst = y.fst → x.snd = y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, rfl => rfl
-
-@[ext] theorem Sigma.ext : {x y : Sigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
-
-@[ext] theorem PSigma.ext : {x y : PSigma β} → x.fst = y.fst → HEq x.snd y.snd → x = y
-  | ⟨_,_⟩, ⟨_,_⟩, rfl, .rfl => rfl
-
-@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
-protected theorem Unit.ext (x y : Unit) : x = y := rfl

src/Init/Notation.lean

@@ -464,14 +464,6 @@ macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
 namespace Lean
 
-/--
-* The `by_elab doSeq` expression runs the `doSeq` as a `TermElabM Expr` to
-  synthesize the expression.
-* `by_elab fun expectedType? => do doSeq` receives the expected type (an `Option Expr`)
-  as well.
--/
-syntax (name := byElab) "by_elab " doSeq : term
-
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.
@@ -506,26 +498,3 @@ a string literal with the contents of the file at `"parent_dir" / "path" / "to"
 file cannot be read, elaboration fails.
 -/
 syntax (name := includeStr) "include_str " term : term
-
-/--
-The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
-This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
--/
-syntax (name := runCmd) "run_cmd " doSeq : command
-
-/--
-The `run_elab doSeq` command executes code in `TermElabM Unit`.
-This is almost the same as `#eval show TermElabM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
--/
-syntax (name := runElab) "run_elab " doSeq : command
-
-/--
-The `run_meta doSeq` command executes code in `MetaM Unit`.
-This is almost the same as `#eval show MetaM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
-
-(This is effectively a synonym for `run_elab`.)
--/
-syntax (name := runMeta) "run_meta " doSeq : command

src/Init/NotationExtra.lean

@@ -391,23 +391,6 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
-macro_rules
-  | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
-  | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body)
-  | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body)
-  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body)
-  | `(haveI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
-
-macro_rules
-  | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
-  | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body)
-  | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body)
-  | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
-  | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
-
-
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic

src/Init/Prelude.lean

@@ -548,11 +548,6 @@ theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :
   | Or.inl h => left h
   | Or.inr h => right h
 
-theorem Or.resolve_left  (h: Or a b) (na : Not a) : b := h.elim (absurd · na) id
-theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb)
-theorem Or.neg_resolve_left  (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id
-theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)
-
 /--
 `Bool` is the type of boolean values, `true` and `false`. Classically,
 this is equivalent to `Prop` (the type of propositions), but the distinction

src/Init/PropLemmas.lean

@@ -1,437 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO.  All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
-
-This provides additional lemmas about propositional types beyond what is
-needed for Core and SimpLemmas.
--/
-prelude
-import Init.Core
-import Init.NotationExtra
-set_option linter.missingDocs true -- keep it documented
-
-/-! ## not -/
-
-theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))
-
-/-! ## and -/
-
-theorem and_self_iff : a ∧ a ↔ a := Iff.of_eq (and_self a)
-theorem and_not_self_iff (a : Prop) : a ∧ ¬a ↔ False := iff_false_intro and_not_self
-theorem not_and_self_iff (a : Prop) : ¬a ∧ a ↔ False := iff_false_intro not_and_self
-
-theorem And.imp (f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d :=  And.intro (f h.left) (g h.right)
-theorem And.imp_left (h : a → b) : a ∧ c → b ∧ c := .imp h id
-theorem And.imp_right (h : a → b) : c ∧ a → c ∧ b := .imp id h
-
-theorem and_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d :=
-  Iff.intro (And.imp h₁.mp h₂.mp) (And.imp h₁.mpr h₂.mpr)
-theorem and_congr_left' (h : a ↔ b) : a ∧ c ↔ b ∧ c := and_congr h .rfl
-theorem and_congr_right' (h : b ↔ c) : a ∧ b ↔ a ∧ c := and_congr .rfl h
-
-theorem not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) := mt And.left
-theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := mt And.right
-
-theorem and_congr_right_eq (h : a → b = c) : (a ∧ b) = (a ∧ c) :=
-  propext (and_congr_right (Iff.of_eq ∘ h))
-theorem and_congr_left_eq  (h : c → a = b) : (a ∧ c) = (b ∧ c) :=
-  propext (and_congr_left  (Iff.of_eq ∘ h))
-
-theorem and_left_comm : a ∧ b ∧ c ↔ b ∧ a ∧ c :=
-  Iff.intro (fun ⟨ha, hb, hc⟩ => ⟨hb, ha, hc⟩)
-            (fun ⟨hb, ha, hc⟩ => ⟨ha, hb, hc⟩)
-
-theorem and_right_comm : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
-  Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨⟨ha, hc⟩, hb⟩)
-            (fun ⟨⟨ha, hc⟩, hb⟩ => ⟨⟨ha, hb⟩, hc⟩)
-
-theorem and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a := by rw [and_left_comm, @and_comm a c]
-theorem and_and_and_comm : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d := by rw [← and_assoc, @and_right_comm a, and_assoc]
-theorem and_and_left  : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c := by rw [and_and_and_comm, and_self]
-theorem and_and_right : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c := by rw [and_and_and_comm, and_self]
-
-theorem and_iff_left  (hb : b) : a ∧ b ↔ a := Iff.intro And.left  (And.intro · hb)
-theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro ha ·)
-
-/-! ## or -/
-
-theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl
-theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb)
-
-theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩
-theorem or_congr_left (h : a ↔ b) : a ∨ c ↔ b ∨ c := or_congr h .rfl
-theorem or_congr_right (h : b ↔ c) : a ∨ b ↔ a ∨ c := or_congr .rfl h
-
-theorem or_left_comm  : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := by rw [← or_assoc, ← or_assoc, @or_comm a b]
-theorem or_right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, @or_comm b]
-
-theorem or_or_or_comm : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d := by rw [← or_assoc, @or_right_comm a, or_assoc]
-
-theorem or_or_distrib_left : a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c := by rw [or_or_or_comm, or_self]
-theorem or_or_distrib_right : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c := by rw [or_or_or_comm, or_self]
-
-theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_comm, Or.comm]
-
-theorem or_iff_left  (hb : ¬b) : a ∨ b ↔ a := or_iff_left_iff_imp.mpr  hb.elim
-theorem or_iff_right (ha : ¬a) : a ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elim
-
-/-! ## distributivity -/
-
-theorem not_imp_of_and_not : a ∧ ¬b → ¬(a → b)
-  | ⟨ha, hb⟩, h => hb <| h ha
-
-theorem imp_and {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
-  ⟨fun h => ⟨fun ha => (h ha).1, fun ha => (h ha).2⟩, fun h ha => ⟨h.1 ha, h.2 ha⟩⟩
-
-theorem not_and' : ¬(a ∧ b) ↔ b → ¬a := Iff.trans not_and imp_not_comm
-
-/-- `∧` distributes over `∨` (on the left). -/
-theorem and_or_left : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) :=
-  Iff.intro (fun ⟨ha, hbc⟩ => hbc.imp (.intro ha) (.intro ha))
-            (Or.rec (.imp_right .inl) (.imp_right .inr))
-
-/-- `∧` distributes over `∨` (on the right). -/
-theorem or_and_right : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := by rw [@and_comm (a ∨ b), and_or_left, @and_comm c, @and_comm c]
-
-/-- `∨` distributes over `∧` (on the left). -/
-theorem or_and_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) :=
-  Iff.intro (Or.rec (fun ha => ⟨.inl ha, .inl ha⟩) (.imp .inr .inr))
-            (And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro))
-
-/-- `∨` distributes over `∧` (on the right). -/
-theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or_comm (a ∧ b), or_and_left, @or_comm c, @or_comm c]
-
-theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
-  Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)
-theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
-
-theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
-
-/-! ## exists and forall -/
-
-section quantifiers
-variable {p q : α → Prop} {b : Prop}
-
-theorem forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a := fun h' a => h a (h' a)
-
-/--
-As `simp` does not index foralls, this `@[simp]` lemma is tried on every `forall` expression.
-This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time.
--/
-@[simp] theorem forall_exists_index {q : (∃ x, p x) → Prop} :
-    (∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩ :=
-  ⟨fun h x hpx => h ⟨x, hpx⟩, fun h ⟨x, hpx⟩ => h x hpx⟩
-
-theorem Exists.imp (h : ∀ a, p a → q a) : (∃ a, p a) → ∃ a, q a
-  | ⟨a, hp⟩ => ⟨a, h a hp⟩
-
-theorem Exists.imp' {β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a)) :
-    (∃ a, p a) → ∃ b, q b
-  | ⟨_, hp⟩ => ⟨_, hpq _ hp⟩
-
-theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_index
-
-@[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
-  ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩
-
-section forall_congr
-
-theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a :=
-  ⟨fun H a => (h a).1 (H a), fun H a => (h a).2 (H a)⟩
-
-theorem exists_congr (h : ∀ a, p a ↔ q a) : (∃ a, p a) ↔ ∃ a, q a :=
-  ⟨Exists.imp fun x => (h x).1, Exists.imp fun x => (h x).2⟩
-
-variable {β : α → Sort _}
-
-theorem forall₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
-    (∀ a b, p a b) ↔ ∀ a b, q a b :=
-  forall_congr' fun a => forall_congr' <| h a
-
-theorem exists₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
-    (∃ a b, p a b) ↔ ∃ a b, q a b :=
-  exists_congr fun a => exists_congr <| h a
-
-variable {γ : ∀ a, β a → Sort _}
-theorem forall₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
-    (∀ a b c, p a b c) ↔ ∀ a b c, q a b c :=
-  forall_congr' fun a => forall₂_congr <| h a
-
-theorem exists₃_congr {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
-    (∃ a b c, p a b c) ↔ ∃ a b c, q a b c :=
-  exists_congr fun a => exists₂_congr <| h a
-
-variable {δ : ∀ a b, γ a b → Sort _}
-theorem forall₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
-    (∀ a b c d, p a b c d) ↔ ∀ a b c d, q a b c d :=
-  forall_congr' fun a => forall₃_congr <| h a
-
-theorem exists₄_congr {p q : ∀ a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
-    (∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d :=
-  exists_congr fun a => exists₃_congr <| h a
-
-variable {ε : ∀ a b c, δ a b c → Sort _}
-theorem forall₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
-    (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
-    (∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e :=
-  forall_congr' fun a => forall₄_congr <| h a
-
-theorem exists₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
-    (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
-    (∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e :=
-  exists_congr fun a => exists₄_congr <| h a
-
-end forall_congr
-
-@[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_imp
-
-theorem forall_and : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
-  ⟨fun h => ⟨fun x => (h x).1, fun x => (h x).2⟩, fun ⟨h₁, h₂⟩ x => ⟨h₁ x, h₂ x⟩⟩
-
-theorem exists_or : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x :=
-  ⟨fun | ⟨x, .inl h⟩ => .inl ⟨x, h⟩ | ⟨x, .inr h⟩ => .inr ⟨x, h⟩,
-   fun | .inl ⟨x, h⟩ => ⟨x, .inl h⟩ | .inr ⟨x, h⟩ => ⟨x, .inr h⟩⟩
-
-@[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => h
-
-@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
-  ⟨i.elim, fun hb _ => hb⟩
-
-theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩
-
-theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x
-  | ⟨x, hn⟩, h => hn (h x)
-
-@[simp] theorem forall_eq {p : α → Prop} {a' : α} : (∀ a, a = a' → p a) ↔ p a' :=
-  ⟨fun h => h a' rfl, fun h _ e => e.symm ▸ h⟩
-
-@[simp] theorem forall_eq' {a' : α} : (∀ a, a' = a → p a) ↔ p a' := by simp [@eq_comm _ a']
-
-@[simp] theorem exists_eq : ∃ a, a = a' := ⟨_, rfl⟩
-
-@[simp] theorem exists_eq' : ∃ a, a' = a := ⟨_, rfl⟩
-
-@[simp] theorem exists_eq_left : (∃ a, a = a' ∧ p a) ↔ p a' :=
-  ⟨fun ⟨_, e, h⟩ => e ▸ h, fun h => ⟨_, rfl, h⟩⟩
-
-@[simp] theorem exists_eq_right : (∃ a, p a ∧ a = a') ↔ p a' :=
-  (exists_congr <| by exact fun a => And.comm).trans exists_eq_left
-
-@[simp] theorem exists_and_left : (∃ x, b ∧ p x) ↔ b ∧ (∃ x, p x) :=
-  ⟨fun ⟨x, h, hp⟩ => ⟨h, x, hp⟩, fun ⟨h, x, hp⟩ => ⟨x, h, hp⟩⟩
-
-@[simp] theorem exists_and_right : (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b := by simp [And.comm]
-
-@[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a']
-
-@[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by
-  simp only [or_imp, forall_and, forall_eq]
-
-@[simp] theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by
-  simp only [or_and_right, exists_or, exists_eq_left]
-
-@[simp] theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a' := by
-  simp [← and_assoc]
-
-@[simp] theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a' := by
-  simp [@eq_comm _ a']
-
-@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
-  ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
-
-@[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩
-
-theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
-  @forall_const (q h) p ⟨h⟩
-
-theorem forall_comm {p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b) :=
-  ⟨fun h b a => h a b, fun h a b => h b a⟩
-
-theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b) :=
-  ⟨fun ⟨a, b, h⟩ => ⟨b, a, h⟩, fun ⟨b, a, h⟩ => ⟨a, b, h⟩⟩
-
-@[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
-    (∀ b a, f a = b → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]
-
-@[simp] theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} :
-    (∀ b a, b = f a → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]
-
-@[simp] theorem forall_apply_eq_imp_iff₂ {f : α → β} {p : α → Prop} {q : β → Prop} :
-    (∀ b a, p a → f a = b → q b) ↔ ∀ a, p a → q (f a) :=
-  ⟨fun h a ha => h (f a) a ha rfl, fun h _ a ha hb => hb ▸ h a ha⟩
-
-theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
-  iff_true_intro fun h => hn.elim h
-
-end quantifiers
-
-/-! ## decidable -/
-
-theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
-
-theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not
-
-/-- Construct a non-Prop by cases on an `Or`, when the left conjunct is decidable. -/
-protected def Or.by_cases [Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
-  if hp : p then h₁ hp else h₂ (h.resolve_left hp)
-
-/-- Construct a non-Prop by cases on an `Or`, when the right conjunct is decidable. -/
-protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
-  if hq : q then h₂ hq else h₁ (h.resolve_right hq)
-
-instance exists_prop_decidable {p} (P : p → Prop)
-  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
-if h : p then
-  decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
-else isFalse fun ⟨h', _⟩ => h h'
-
-instance forall_prop_decidable {p} (P : p → Prop)
-  [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
-if h : p then
-  decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩
-else isTrue fun h2 => absurd h2 h
-
-theorem decide_eq_true_iff (p : Prop) [Decidable p] : (decide p = true) ↔ p := by simp
-
-@[simp] theorem decide_eq_false_iff_not (p : Prop) {_ : Decidable p} : (decide p = false) ↔ ¬p :=
-  ⟨of_decide_eq_false, decide_eq_false⟩
-
-@[simp] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
-    decide p = decide q ↔ (p ↔ q) :=
-  ⟨fun h => by rw [← decide_eq_true_iff p, h, decide_eq_true_iff], fun h => by simp [h]⟩
-
-theorem Decidable.of_not_imp [Decidable a] (h : ¬(a → b)) : a :=
-  byContradiction (not_not_of_not_imp h)
-
-theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
-  byContradiction <| hb ∘ h
-
-theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
-  ⟨not_imp_symm, not_imp_symm⟩
-
-theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
-  have := @imp_not_self (¬a); rwa [not_not] at this
-
-theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=
-  ⟨Or.resolve_left, fun h => dite _ .inl (.inr ∘ h)⟩
-
-theorem Decidable.or_iff_not_imp_right [Decidable b] : a ∨ b ↔ (¬b → a) :=
-  or_comm.trans or_iff_not_imp_left
-
-theorem Decidable.not_imp_not [Decidable a] : (¬a → ¬b) ↔ (b → a) :=
-  ⟨fun h hb => byContradiction (h · hb), mt⟩
-
-theorem Decidable.not_or_of_imp [Decidable a] (h : a → b) : ¬a ∨ b :=
-  if ha : a then .inr (h ha) else .inl ha
-
-theorem Decidable.imp_iff_not_or [Decidable a] : (a → b) ↔ (¬a ∨ b) :=
-  ⟨not_or_of_imp, Or.neg_resolve_left⟩
-
-theorem Decidable.imp_iff_or_not [Decidable b] : b → a ↔ a ∨ ¬b :=
-  Decidable.imp_iff_not_or.trans or_comm
-
-theorem Decidable.imp_or [h : Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
-  if h : a then by
-    rw [imp_iff_right h, imp_iff_right h, imp_iff_right h]
-  else by
-    rw [iff_false_intro h, false_imp_iff, false_imp_iff, true_or]
-
-theorem Decidable.imp_or' [Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
-  if h : b then by simp [h] else by
-    rw [eq_false h, false_or]; exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm
-
-theorem Decidable.not_imp_iff_and_not [Decidable a] : ¬(a → b) ↔ a ∧ ¬b :=
-  ⟨fun h => ⟨of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩
-
-theorem Decidable.peirce (a b : Prop) [Decidable a] : ((a → b) → a) → a :=
-  if ha : a then fun _ => ha else fun h => h ha.elim
-
-theorem peirce' {a : Prop} (H : ∀ b : Prop, (a → b) → a) : a := H _ id
-
-theorem Decidable.not_iff_not [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b) := by
-  rw [@iff_def (¬a), @iff_def' a]; exact and_congr not_imp_not not_imp_not
-
-theorem Decidable.not_iff_comm [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a) := by
-  rw [@iff_def (¬a), @iff_def (¬b)]; exact and_congr not_imp_comm imp_not_comm
-
-theorem Decidable.not_iff [Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b) :=
-  if h : b then by
-    rw [iff_true_right h, iff_true_right h]
-  else by
-    rw [iff_false_right h, iff_false_right h]
-
-theorem Decidable.iff_not_comm [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a) := by
-  rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm not_imp_comm
-
-theorem Decidable.iff_iff_and_or_not_and_not {a b : Prop} [Decidable b] :
-    (a ↔ b) ↔ (a ∧ b) ∨ (¬a ∧ ¬b) :=
-  ⟨fun e => if h : b then .inl ⟨e.2 h, h⟩ else .inr ⟨mt e.1 h, h⟩,
-   Or.rec (And.rec iff_of_true) (And.rec iff_of_false)⟩
-
-theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] :
-    (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by
-  rw [iff_iff_implies_and_implies a b]; simp only [imp_iff_not_or, Or.comm]
-
-theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b) :=
-  ⟨fun h ha => not_imp_symm (And.intro ha) h, fun h ⟨ha, hb⟩ => hb <| h ha⟩
-
-theorem Decidable.not_and_iff_or_not_not [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
-  ⟨fun h => if ha : a then .inr (h ⟨ha, ·⟩) else .inl ha, not_and_of_not_or_not⟩
-
-theorem Decidable.not_and_iff_or_not_not' [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
-  ⟨fun h => if hb : b then .inl (h ⟨·, hb⟩) else .inr hb, not_and_of_not_or_not⟩
-
-theorem Decidable.or_iff_not_and_not [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b) := by
-  rw [← not_or, not_not]
-
-theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b) := by
-  rw [← not_and_iff_or_not_not, not_not]
-
-theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
-  ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
-   fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩
-
-theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
-  if ha : a then by simp only [ha, true_and, true_imp_iff]
-  else by simp only [ha, false_or, false_and, false_imp_iff]
-
-theorem Decidable.or_congr_left' [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c := by
-  rw [or_iff_not_imp_right, or_iff_not_imp_right]; exact imp_congr_right h
-
-theorem Decidable.or_congr_right' [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c := by
-  rw [or_iff_not_imp_left, or_iff_not_imp_left]; exact imp_congr_right h
-
-/-- Transfer decidability of `a` to decidability of `b`, if the propositions are equivalent.
-**Important**: this function should be used instead of `rw` on `Decidable b`, because the
-kernel will get stuck reducing the usage of `propext` otherwise,
-and `decide` will not work. -/
-@[inline] def decidable_of_iff (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
-  decidable_of_decidable_of_iff h
-
-/-- Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent.
-This is the same as `decidable_of_iff` but the iff is flipped. -/
-@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a :=
-  decidable_of_decidable_of_iff h.symm
-
-instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
-    CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩
-
-/-- Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`.
-(This is sometimes taken as an alternate definition of decidability.) -/
-def decidable_of_bool : ∀ (b : Bool), (b ↔ a) → Decidable a
-  | true, h => isTrue (h.1 rfl)
-  | false, h => isFalse (mt h.2 Bool.noConfusion)
-
-protected theorem Decidable.not_forall {p : α → Prop} [Decidable (∃ x, ¬p x)]
-    [∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x :=
-  ⟨Decidable.not_imp_symm fun nx x => Decidable.not_imp_symm (fun h => ⟨x, h⟩) nx,
-   not_forall_of_exists_not⟩
-
-protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x, p x)] :
-    (¬∀ x, ¬p x) ↔ ∃ x, p x :=
-  (@Decidable.not_iff_comm _ _ _ (decidable_of_iff (¬∃ x, p x) not_exists)).1 not_exists
-
-protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
-    (¬∃ x, ¬p x) ↔ ∀ x, p x := by
-  simp only [not_exists, Decidable.not_not]

src/Init/SimpLemmas.lean

@@ -31,9 +31,6 @@ theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) :
 theorem implies_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   h₁ ▸ h₂ ▸ rfl
 
-theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
-  Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
-
 theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : (h : p₂) → q₁ = q₂ h) : (p₁ → q₁) = ((h : p₂) → q₂ h) :=
   propext ⟨
     fun hl hp₂ => (h₂ hp₂).mp (hl (h₁.mpr hp₂)),
@@ -96,16 +93,11 @@ theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c →
 theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]
 end SimprocHelperLemmas
 @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl
-
+@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩
 @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1)
-@[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩
-@[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn
-@[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm
-@[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
-@[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩
 @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)
 @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial)
@@ -122,58 +114,6 @@ end SimprocHelperLemmas
 @[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
 @[simp] theorem not_true_eq_false : (¬ True) = False := by decide
 
-@[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm
-
-/-! ## and -/
-
-theorem and_congr_right (h : a → (b ↔ c)) : a ∧ b ↔ a ∧ c :=
-  Iff.intro (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mp hb))
-            (fun ⟨ha, hb⟩ => And.intro ha ((h ha).mpr hb))
-theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=
-  Iff.trans and_comm (Iff.trans (and_congr_right h) and_comm)
-
-theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
-  Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
-            (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)
-
-@[simp] theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]
-@[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]
-
-@[simp] theorem and_congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
-  Iff.intro (fun h ha => by simp [ha] at h; exact h) and_congr_right
-@[simp] theorem and_congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b) := by
-  rw [@and_comm _ c, @and_comm _ c, ← and_congr_right_iff]
-
-theorem and_iff_left_of_imp  (h : a → b) : (a ∧ b) ↔ a := Iff.intro And.left (fun ha => And.intro ha (h ha))
-theorem and_iff_right_of_imp (h : b → a) : (a ∧ b) ↔ b := Iff.trans And.comm (and_iff_left_of_imp h)
-
-@[simp] theorem and_iff_left_iff_imp  : ((a ∧ b) ↔ a) ↔ (a → b) := Iff.intro (And.right ∘ ·.mpr) and_iff_left_of_imp
-@[simp] theorem and_iff_right_iff_imp : ((a ∧ b) ↔ b) ↔ (b → a) := Iff.intro (And.left ∘ ·.mpr) and_iff_right_of_imp
-
-@[simp] theorem iff_self_and : (p ↔ p ∧ q) ↔ (p → q) := by rw [@Iff.comm p, and_iff_left_iff_imp]
-@[simp] theorem iff_and_self : (p ↔ q ∧ p) ↔ (p → q) := by rw [and_comm, iff_self_and]
-
-/-! ## or -/
-
-theorem Or.imp (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d := h.elim (inl ∘ f) (inr ∘ g)
-theorem Or.imp_left (f : a → b) : a ∨ c → b ∨ c := .imp f id
-theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f
-
-theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
-  Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr))
-            (.rec (.inl ∘ .inl) (.imp_left .inr))
-
-@[simp] theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]
-@[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]
-
-theorem or_iff_right_of_imp (ha : a → b) : (a ∨ b) ↔ b := Iff.intro (Or.rec ha id) .inr
-theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.rec id hb) .inl
-
-@[simp] theorem or_iff_left_iff_imp  : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp
-@[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]
-
-/-# Bool -/
-
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
 @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b  := by cases b <;> rfl
@@ -226,13 +166,11 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
 @[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
 
+@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
+  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩
+
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
 
 @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
   simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]
-
-/-# Nat -/
-
-@[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
-  propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by rw [h]; decide⟩

src/Init/Tactics.lean

@@ -398,7 +398,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
+syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
 
 /--
 Location specifications are used by many tactics that can operate on either the
@@ -894,37 +894,6 @@ The tactic `nomatch h` is shorthand for `exact nomatch h`.
 macro "nomatch " es:term,+ : tactic =>
   `(tactic| exact nomatch $es:term,*)
 
-/--
-Acts like `have`, but removes a hypothesis with the same name as
-this one if possible. For example, if the state is:
-
-```lean
-f : α → β
-h : α
-⊢ goal
-```
-
-Then after `replace h := f h` the state will be:
-
-```lean
-f : α → β
-h : β
-⊢ goal
-```
-
-whereas `have h := f h` would result in:
-
-```lean
-f : α → β
-h† : α
-h : β
-⊢ goal
-```
-
-This can be used to simulate the `specialize` and `apply at` tactics of Coq.
--/
-syntax (name := replace) "replace" haveDecl : tactic
-
 /--
 `repeat' tac` runs `tac` on all of the goals to produce a new list of goals,
 then runs `tac` again on all of those goals, and repeats until `tac` fails on all remaining goals.
@@ -941,21 +910,6 @@ syntax (name := repeat1') "repeat1' " tacticSeq : tactic
 syntax "and_intros" : tactic
 macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 
-/--
-`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
-replacing the left side of the equality with the right, until no more progress can be made.
--/
-syntax (name := substEqs) "subst_eqs" : tactic
-
-/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
-syntax (name := runTac) "run_tac " doSeq : tactic
-
-/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
-
-/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
-
 end Tactic
 
 namespace Attr

src/Init/WF.lean

@@ -206,39 +206,12 @@ protected inductive Lex : α × β → α × β → Prop where
   | left  {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Prod.Lex (a₁, b₁) (a₂, b₂)
   | right (a) {b₁ b₂} (h : rb b₁ b₂)         : Prod.Lex (a, b₁)  (a, b₂)
 
-theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
-    Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
-  ⟨fun h => by cases h <;> simp [*], fun h =>
-    match p, q, h with
-    | (a, b), (c, d), Or.inl h => Lex.left _ _ h
-    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
-
-namespace Lex
-
-instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRel r]
-    {s : β → β → Prop} [sDec : DecidableRel s] : DecidableRel (Prod.Lex r s)
-  | (a, b), (a', b') =>
-    match rDec a a' with
-    | isTrue raa' => isTrue $ left b b' raa'
-    | isFalse nraa' =>
-      match αeqDec a a' with
-      | isTrue eq => by
-        subst eq
-        cases sDec b b' with
-        | isTrue sbb' => exact isTrue $ right a sbb'
-        | isFalse nsbb' =>
-          apply isFalse; intro contra; cases contra <;> contradiction
-      | isFalse neqaa' => by
-        apply isFalse; intro contra; cases contra <;> contradiction
-
 -- TODO: generalize
-def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+def Lex.right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
 
-end Lex
-
 -- relational product based on ra and rb
 inductive RProd : α × β → α × β → Prop where
   | intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : RProd (a₁, b₁) (a₂, b₂)

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -25,13 +25,9 @@ def leanMainFn := "_lean_main"
 
 namespace LLVM
 -- TODO(bollu): instantiate target triple and find out what size_t is.
-def size_tType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
+def size_tType (llvmctx : LLVM.Context) : IO (LLVM.LLVMType llvmctx) :=
   LLVM.i64Type llvmctx
 
--- TODO(bollu): instantiate target triple and find out what unsigned is.
-def unsignedType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) :=
-  LLVM.i32Type llvmctx
-
 -- Helper to add a function if it does not exist, and to return the function handle if it does.
 def getOrAddFunction (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx) :=  do
   match (← LLVM.getNamedFunction m name) with
@@ -100,15 +96,6 @@ def getDecl (n : Name) : M llvmctx Decl := do
   | some d => pure d
   | none   => throw s!"unknown declaration {n}"
 
-def constInt8 (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constInt8 llvmctx (UInt64.ofNat n)
-
-def constInt64 (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constInt64 llvmctx (UInt64.ofNat n)
-
-def constIntSizeT (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
-    LLVM.constIntSizeT llvmctx (UInt64.ofNat n)
-
 def constIntUnsigned (n : Nat) : M llvmctx (LLVM.Value llvmctx) :=  do
     LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
 
@@ -175,14 +162,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
   let retty ← LLVM.voidPtrType llvmctx
   let f ←   getOrCreateFunctionPrototype mod retty "lean_unsigned_to_nat"  argtys
   let fnty ← LLVM.functionType retty argtys
-  let nv ← constIntUnsigned n
+  let nv ← LLVM.constInt32 llvmctx (UInt64.ofNat n)
   LLVM.buildCall2 builder fnty f #[nv] name
 
 def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
     (strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_mk_string_from_bytes"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.i64Type llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
@@ -231,9 +218,9 @@ def callLeanAllocCtor (builder : LLVM.Builder llvmctx)
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
 
-  let tag ← constIntUnsigned tag
-  let num_objs ← constIntUnsigned num_objs
-  let scalar_sz ← constIntUnsigned scalar_sz
+  let tag ← LLVM.constInt32 llvmctx (UInt64.ofNat tag)
+  let num_objs ← LLVM.constInt32 llvmctx (UInt64.ofNat num_objs)
+  let scalar_sz ← LLVM.constInt32 llvmctx (UInt64.ofNat scalar_sz)
   LLVM.buildCall2 builder fnty fn #[tag, num_objs, scalar_sz] name
 
 def callLeanCtorSet (builder : LLVM.Builder llvmctx)
@@ -241,7 +228,7 @@ def callLeanCtorSet (builder : LLVM.Builder llvmctx)
   let fnName := "lean_ctor_set"
   let retty ← LLVM.voidType llvmctx
   let voidptr ← LLVM.voidPtrType llvmctx
-  let unsigned ← LLVM.unsignedType llvmctx
+  let unsigned ← LLVM.size_tType llvmctx
   let argtys :=  #[voidptr, unsigned, voidptr]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
@@ -261,7 +248,7 @@ def callLeanAllocClosureFn (builder : LLVM.Builder llvmctx)
     (f arity nys : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_alloc_closure"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   LLVM.buildCall2 builder fnty fn  #[f, arity, nys] retName
@@ -270,7 +257,7 @@ def callLeanClosureSetFn (builder : LLVM.Builder llvmctx)
     (closure ix arg : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_closure_set"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, ix, arg] retName
@@ -298,7 +285,7 @@ def callLeanCtorRelease (builder : LLVM.Builder llvmctx)
     (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_ctor_release"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, i] retName
@@ -307,7 +294,7 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx)
     (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set_tag"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[closure, i] retName
@@ -360,31 +347,6 @@ def builderAppendBasicBlock (builder : LLVM.Builder llvmctx) (name : String) : M
   let fn ← builderGetInsertionFn builder
   LLVM.appendBasicBlockInContext llvmctx fn name
 
-/--
-Add an alloca to the first BB of the current function. The builders final position
-will be the end of the BB that we came from.
-
-If it is possible to put an alloca in the first BB this approach is to be preferred
-over putting it in other BBs. This is because mem2reg only inspects allocas in the first BB,
-leading to missed optimizations for allocas in other BBs.
--/
-def buildPrologueAlloca (builder : LLVM.Builder llvmctx) (ty : LLVM.LLVMType llvmctx) (name : @&String := "") : M llvmctx (LLVM.Value llvmctx) := do
-  let origBB ← LLVM.getInsertBlock builder
-
-  let fn ← builderGetInsertionFn builder
-  if (← LLVM.countBasicBlocks fn) == 0 then
-    throw "Attempt to obtain first BB of function without BBs"
-
-  let entryBB ← LLVM.getEntryBasicBlock fn
-  match ← LLVM.getFirstInstruction entryBB with
-  | some instr => LLVM.positionBuilderBefore builder instr
-  | none => LLVM.positionBuilderAtEnd builder entryBB
-
-  let alloca ← LLVM.buildAlloca builder ty name
-  LLVM.positionBuilderAtEnd builder origBB
-  return alloca
-
-
 def buildWhile_ (builder : LLVM.Builder llvmctx) (name : String)
     (condcodegen : LLVM.Builder llvmctx → M llvmctx (LLVM.Value llvmctx))
     (bodycodegen : LLVM.Builder llvmctx → M llvmctx Unit) : M llvmctx Unit := do
@@ -466,7 +428,7 @@ def buildIfThenElse_ (builder : LLVM.Builder llvmctx)  (name : String) (brval :
 -- Recall that lean uses `i8` for booleans, not `i1`, so we need to compare with `true`.
 def buildLeanBoolTrue? (builder : LLVM.Builder llvmctx)
     (b : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx) := do
-  LLVM.buildICmp builder LLVM.IntPredicate.NE b (← constInt8 0) name
+  LLVM.buildICmp builder LLVM.IntPredicate.NE b (← LLVM.constInt8 llvmctx 0) name
 
 def emitFnDeclAux (mod : LLVM.Module llvmctx)
     (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M llvmctx (LLVM.Value llvmctx) := do
@@ -551,8 +513,8 @@ def emitArgSlot_ (builder : LLVM.Builder llvmctx)
   | Arg.var x => emitLhsSlot_ x
   | _ => do
     let slotty ← LLVM.voidPtrType llvmctx
-    let slot ← buildPrologueAlloca builder slotty "irrelevant_slot"
-    let v ← callLeanBox builder (← constIntSizeT 0) "irrelevant_val"
+    let slot ← LLVM.buildAlloca builder slotty "irrelevant_slot"
+    let v ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "irrelevant_val"
     let _ ← LLVM.buildStore builder v slot
     return (slotty, slot)
 
@@ -574,7 +536,7 @@ def emitCtorSetArgs (builder : LLVM.Builder llvmctx)
   ys.size.forM fun i => do
     let zv ← emitLhsVal builder z
     let (_yty, yv) ← emitArgVal builder ys[i]!
-    let iv ← constIntUnsigned i
+    let iv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat i)
     callLeanCtorSet builder zv iv yv
     emitLhsSlotStore builder z zv
     pure ()
@@ -583,7 +545,7 @@ def emitCtor (builder : LLVM.Builder llvmctx)
     (z : VarId) (c : CtorInfo) (ys : Array Arg) : M llvmctx Unit := do
   let (_llvmty, slot) ← emitLhsSlot_ z
   if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
-    let v ← callLeanBox builder (← constIntSizeT c.cidx) "lean_box_outv"
+    let v ← callLeanBox builder (← constIntUnsigned c.cidx) "lean_box_outv"
     let _ ← LLVM.buildStore builder v slot
   else do
     let v ← emitAllocCtor builder c
@@ -595,7 +557,7 @@ def emitInc (builder : LLVM.Builder llvmctx)
   let xv ← emitLhsVal builder x
   if n != 1
   then do
-     let nv ← constIntSizeT n
+     let nv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat n)
      callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) (delta := nv) xv
   else callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) xv
 
@@ -709,7 +671,7 @@ def emitPartialApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys
 
 def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array Arg) : M llvmctx Unit := do
   if ys.size > closureMaxArgs then do
-    let aargs ← buildPrologueAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
+    let aargs ← LLVM.buildAlloca builder (← LLVM.arrayType (← LLVM.voidPtrType llvmctx) (UInt64.ofNat ys.size)) "aargs"
     for i in List.range ys.size do
       let (yty, yv) ← emitArgVal builder ys[i]!
       let aslot ← LLVM.buildInBoundsGEP2 builder yty aargs #[← constIntUnsigned 0, ← constIntUnsigned i] s!"param_{i}_slot"
@@ -718,7 +680,7 @@ def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array
     let retty ← LLVM.voidPtrType llvmctx
     let args := #[← emitLhsVal builder f, ← constIntUnsigned ys.size, aargs]
     -- '1 + ...'. '1' for the fn and 'args' for the arguments
-    let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx]
+    let argtys := #[← LLVM.voidPtrType llvmctx]
     let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
     let fnty ← LLVM.functionType retty argtys
     let zv ← LLVM.buildCall2 builder fnty fn args
@@ -760,18 +722,18 @@ def emitFullApp (builder : LLVM.Builder llvmctx)
 def emitLit (builder : LLVM.Builder llvmctx)
     (z : VarId) (t : IRType) (v : LitVal) : M llvmctx (LLVM.Value llvmctx) := do
   let llvmty ← toLLVMType t
-  let zslot ← buildPrologueAlloca builder llvmty
+  let zslot ← LLVM.buildAlloca builder llvmty
   addVartoState z zslot llvmty
   let zv ← match v with
             | LitVal.num v => emitNumLit builder t v
             | LitVal.str v =>
-                 let zero ← constIntUnsigned 0
+                 let zero ← LLVM.constIntUnsigned llvmctx 0
                  let str_global ← LLVM.buildGlobalString builder v
                  -- access through the global, into the 0th index of the array
                  let strPtr ← LLVM.buildInBoundsGEP2 builder
                                 (← LLVM.opaquePointerTypeInContext llvmctx)
                                 str_global #[zero] ""
-                 let nbytes ← constIntSizeT v.utf8ByteSize
+                 let nbytes ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat (v.utf8ByteSize))
                  callLeanMkStringFromBytesFn builder strPtr nbytes ""
   LLVM.buildStore builder zv zslot
   return zslot
@@ -795,7 +757,7 @@ def callLeanCtorGetUsize (builder : LLVM.Builder llvmctx)
     (x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx) := do
   let fnName :=  "lean_ctor_get_usize"
   let retty ← LLVM.size_tType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fnty ← LLVM.functionType retty argtys
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   LLVM.buildCall2 builder fnty fn  #[x, i] retName
@@ -822,7 +784,7 @@ def emitSProj (builder : LLVM.Builder llvmctx)
     | IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
     | IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
     | _             => throw s!"Invalid type for lean_ctor_get: '{t}'"
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xval ← emitLhsVal builder x
   let offset ← emitOffset builder n offset
@@ -929,7 +891,7 @@ def emitReset (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId)
    (fun builder => do
       let xv ← emitLhsVal builder x
       callLeanDecRef builder xv
-      let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+      let box0 ← callLeanBox builder (← constIntUnsigned 0) "box0"
       emitLhsSlotStore builder z box0
       return ShouldForwardControlFlow.yes
    )
@@ -950,7 +912,7 @@ def emitReuse (builder : LLVM.Builder llvmctx)
        emitLhsSlotStore builder z xv
        if updtHeader then
           let zv ← emitLhsVal builder z
-          callLeanCtorSetTag builder zv (← constInt8 c.cidx)
+          callLeanCtorSetTag builder zv (← constIntUnsigned c.cidx)
        return ShouldForwardControlFlow.yes
    )
   emitCtorSetArgs builder z ys
@@ -973,7 +935,7 @@ def emitVDecl (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : Exp
 
 def declareVar (builder : LLVM.Builder llvmctx) (x : VarId) (t : IRType) : M llvmctx Unit := do
   let llvmty ← toLLVMType t
-  let alloca ← buildPrologueAlloca builder llvmty "varx"
+  let alloca ← LLVM.buildAlloca builder llvmty "varx"
   addVartoState x alloca llvmty
 
 partial def declareVars (builder : LLVM.Builder llvmctx) (f : FnBody) : M llvmctx Unit := do
@@ -999,7 +961,7 @@ def emitTag (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) : M ll
 def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx , ← LLVM.voidPtrType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitArgVal builder y).2]
@@ -1007,7 +969,7 @@ def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M
 def emitUSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : VarId) : M llvmctx Unit := do
   let fnName :=  "lean_ctor_set_usize"
   let retty ← LLVM.voidType llvmctx
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   let _ ← LLVM.buildCall2 builder fnty fn  #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitLhsVal builder y)]
@@ -1046,7 +1008,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
   | IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
   | IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
   | _             => throw s!"invalid type for 'lean_ctor_set': '{t}'"
-  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
+  let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xv ← emitLhsVal builder x
@@ -1064,12 +1026,12 @@ def emitDel (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit := do
   let _ ← LLVM.buildCall2 builder fnty fn  #[xv]
 
 def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmctx Unit := do
-  let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx]
+  let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_ctor_set_tag" argtys
   let xv ← emitLhsVal builder x
   let fnty ← LLVM.functionType retty argtys
-  let _ ← LLVM.buildCall2 builder fnty fn  #[xv, ← constInt8 i]
+  let _ ← LLVM.buildCall2 builder fnty fn  #[xv, ← constIntUnsigned i]
 
 def ensureHasDefault' (alts : Array Alt) : Array Alt :=
   if alts.any Alt.isDefault then alts
@@ -1095,7 +1057,7 @@ partial def emitCase (builder : LLVM.Builder llvmctx)
     match alt with
     | Alt.ctor c b  =>
        let destbb ← builderAppendBasicBlock builder s!"case_{xType}_{c.name}_{c.cidx}"
-       LLVM.addCase switch (← constIntSizeT c.cidx) destbb
+       LLVM.addCase switch (← constIntUnsigned c.cidx) destbb
        LLVM.positionBuilderAtEnd builder destbb
        emitFnBody builder b
     | Alt.default b =>
@@ -1179,14 +1141,14 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
           -- pv := *(argsi) = *(args + i)
           let pv ← LLVM.buildLoad2 builder llvmty argsi
           -- slot for arg[i] which is always void* ?
-          let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}"
+          let alloca ← LLVM.buildAlloca builder llvmty s!"arg_{i}"
           LLVM.buildStore builder pv alloca
           addVartoState params[i]!.x alloca llvmty
   else
       let n ← LLVM.countParams llvmfn
       for i in (List.range n.toNat) do
         let llvmty ← toLLVMType params[i]!.ty
-        let alloca ← buildPrologueAlloca builder  llvmty s!"arg_{i}"
+        let alloca ← LLVM.buildAlloca builder  llvmty s!"arg_{i}"
         let arg ← LLVM.getParam llvmfn (UInt64.ofNat i)
         let _ ← LLVM.buildStore builder arg alloca
         addVartoState params[i]!.x alloca llvmty
@@ -1338,7 +1300,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v"
   buildIfThen_ builder "isGInitialized" ginit?v
     (fun builder => do
-      let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+      let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
       let out ← callLeanIOResultMKOk builder box0 "retval"
       let _ ← LLVM.buildRet builder out
       pure ShouldForwardControlFlow.no)
@@ -1356,7 +1318,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
     callLeanDecRef builder res
   let decls := getDecls env
   decls.reverse.forM (emitDeclInit builder initFn)
-  let box0 ← callLeanBox builder (← constIntSizeT 0) "box0"
+  let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0"
   let out ← callLeanIOResultMKOk builder box0 "retval"
   let _ ← LLVM.buildRet builder out
 
@@ -1470,15 +1432,15 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   #endif
   -/
   let inty ← LLVM.voidPtrType llvmctx
-  let inslot ← buildPrologueAlloca builder (← LLVM.pointerType inty) "in"
+  let inslot ← LLVM.buildAlloca builder (← LLVM.pointerType inty) "in"
   let resty ← LLVM.voidPtrType llvmctx
-  let res ← buildPrologueAlloca builder (← LLVM.pointerType resty) "res"
+  let res ← LLVM.buildAlloca builder (← LLVM.pointerType resty) "res"
   if usesLeanAPI then callLeanInitialize builder else callLeanInitializeRuntimeModule builder
     /- We disable panic messages because they do not mesh well with extracted closed terms.
         See issue #534. We can remove this workaround after we implement issue #467. -/
   callLeanSetPanicMessages builder (← LLVM.constFalse llvmctx)
   let world ← callLeanIOMkWorld builder
-  let resv ← callModInitFn builder (← getModName) (← constInt8 1) world ((← getModName).toString ++ "_init_out")
+  let resv ← callModInitFn builder (← getModName) (← LLVM.constInt8 llvmctx 1) world ((← getModName).toString ++ "_init_out")
   let _ ← LLVM.buildStore builder resv res
 
   callLeanSetPanicMessages builder (← LLVM.constTrue llvmctx)
@@ -1491,21 +1453,21 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
       callLeanDecRef builder resv
       callLeanInitTaskManager builder
       if xs.size == 2 then
-        let inv ← callLeanBox builder (← constIntSizeT 0) "inv"
+        let inv ← callLeanBox builder (← LLVM.constInt (← LLVM.size_tType llvmctx) 0) "inv"
         let _ ← LLVM.buildStore builder inv inslot
         let ity ← LLVM.size_tType llvmctx
-        let islot ← buildPrologueAlloca builder ity "islot"
+        let islot ← LLVM.buildAlloca builder ity "islot"
         let argcval ← LLVM.getParam main 0
         let argvval ← LLVM.getParam main 1
         LLVM.buildStore builder argcval islot
         buildWhile_ builder "argv"
           (condcodegen := fun builder => do
             let iv ← LLVM.buildLoad2 builder ity islot "iv"
-            let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntSizeT 1) "i_gt_1"
+            let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntUnsigned 1) "i_gt_1"
             return i_gt_1)
           (bodycodegen := fun builder => do
             let iv ← LLVM.buildLoad2 builder ity islot "iv"
-            let iv_next ← LLVM.buildSub builder iv (← constIntSizeT 1) "iv.next"
+            let iv_next ← LLVM.buildSub builder iv (← constIntUnsigned 1) "iv.next"
             LLVM.buildStore builder iv_next islot
             let nv ← callLeanAllocCtor builder 1 2 0 "nv"
             let argv_i_next_slot ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argvval #[iv_next] "argv.i.next.slot"
@@ -1547,7 +1509,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         pure ShouldForwardControlFlow.no
       else do
         callLeanDecRef builder resv
-        let _ ← LLVM.buildRet builder (← constInt64 0)
+        let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 0)
         pure ShouldForwardControlFlow.no
 
     )
@@ -1555,7 +1517,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         let resv ← LLVM.buildLoad2 builder resty res "resv"
         callLeanIOResultShowError builder resv
         callLeanDecRef builder resv
-        let _ ← LLVM.buildRet builder (← constInt64 1)
+        let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 1)
         pure ShouldForwardControlFlow.no)
   -- at the merge
   let _ ← LLVM.buildUnreachable builder
@@ -1630,8 +1592,6 @@ def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit
            let some fn ← LLVM.getNamedFunction emitLLVMCtx.llvmmodule name
               | throw <| IO.Error.userError s!"ERROR: linked module must have function from runtime module: '{name}'"
            LLVM.setLinkage fn LLVM.Linkage.internal
-         if let some err ← LLVM.verifyModule emitLLVMCtx.llvmmodule then
-           throw <| .userError err
          LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath
          LLVM.disposeModule emitLLVMCtx.llvmmodule
   | .error err => throw (IO.Error.userError err)

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -182,18 +182,6 @@ opaque createBuilderInContext (ctx : Context) : BaseIO (Builder ctx)
 @[extern "lean_llvm_append_basic_block_in_context"]
 opaque appendBasicBlockInContext (ctx : Context) (fn :  Value ctx) (name :  @&String) : BaseIO (BasicBlock ctx)
 
-@[extern "lean_llvm_count_basic_blocks"]
-opaque countBasicBlocks (fn : Value ctx) : BaseIO UInt64
-
-@[extern "lean_llvm_get_entry_basic_block"]
-opaque getEntryBasicBlock (fn : Value ctx) : BaseIO (BasicBlock ctx)
-
-@[extern "lean_llvm_get_first_instruction"]
-opaque getFirstInstruction (bb : BasicBlock ctx) : BaseIO (Option (Value ctx))
-
-@[extern "lean_llvm_position_builder_before"]
-opaque positionBuilderBefore (builder : Builder ctx) (instr : Value ctx) : BaseIO Unit
-
 @[extern "lean_llvm_position_builder_at_end"]
 opaque positionBuilderAtEnd (builder : Builder ctx) (bb :  BasicBlock ctx) : BaseIO Unit
 
@@ -338,9 +326,6 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit
 @[extern "lean_llvm_dispose_module"]
 opaque disposeModule (m : Module ctx) : BaseIO Unit
 
-@[extern "lean_llvm_verify_module"]
-opaque verifyModule (m : Module ctx) : BaseIO (Option String)
-
 @[extern "lean_llvm_create_string_attribute"]
 opaque createStringAttribute (key : String) (value : String) : BaseIO (Attribute ctx)
 
@@ -454,11 +439,6 @@ def constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : B
 def constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
   constInt' ctx 64 value signExtend
 
-def constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
-  -- TODO: make this stick to the actual size_t of the target machine
-  constInt' ctx 64 value signExtend
-
 def constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) :=
-  -- TODO: make this stick to the actual unsigned of the target machine
-  constInt' ctx 32 value signExtend
+  constInt' ctx 64 value signExtend
 end LLVM

src/Lean/Elab.lean

@@ -10,7 +10,6 @@ import Lean.Elab.Command
 import Lean.Elab.Term
 import Lean.Elab.App
 import Lean.Elab.Binders
-import Lean.Elab.BinderPredicates
 import Lean.Elab.LetRec
 import Lean.Elab.Frontend
 import Lean.Elab.BuiltinNotation

src/Lean/Elab/BinderPredicates.lean

@@ -1,41 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-import Lean.Parser.Syntax
-import Lean.Elab.MacroArgUtil
-import Lean.Linter.MissingDocs
-
-namespace Lean.Elab.Command
-
-@[builtin_command_elab binderPredicate] def elabBinderPred : CommandElab := fun stx => do
-  match stx with
-  | `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind binder_predicate%$tk
-      $[(name := $name?)]? $[(priority := $prio?)]? $x $args:macroArg* => $rhs) => do
-    let prio ← liftMacroM do evalOptPrio prio?
-    let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
-    let name ← match name? with
-      | some name => pure name.getId
-      | none => liftMacroM do mkNameFromParserSyntax `binderTerm (mkNullNode stxParts)
-    let nameTk := name?.getD (mkIdentFrom tk name)
-    /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
-    So, we must include current namespace when we create a pattern for the following
-    `macro_rules` commands. -/
-    let pat : TSyntax `binderPred := ⟨(mkNode ((← getCurrNamespace) ++ name) patArgs).1⟩
-    elabCommand <|<-
-    `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax%$tk
-        (name := $nameTk) (priority := $(quote prio)) $[$stxParts]* : binderPred
-      $[$doc?:docComment]? macro_rules%$tk
-        | `(satisfies_binder_pred% $$($x):term $pat:binderPred) => $rhs)
-  | _ => throwUnsupportedSyntax
-
-open Linter.MissingDocs Parser Term in
-/-- Missing docs handler for `binder_predicate` -/
-@[builtin_missing_docs_handler Lean.Parser.Command.binderPredicate]
-def checkBinderPredicate : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
-    if stx[4].isNone then lint stx[3] "binder predicate"
-    else lintNamed stx[4][0][3] "binder predicate"
-
-end Lean.Elab.Command

src/Lean/Elab/BuiltinCommand.lean

@@ -656,40 +656,35 @@ unsafe def elabEvalUnsafe : CommandElab
         return e
     -- Evaluate using term using `MetaEval` class.
     let elabMetaEval : CommandElabM Unit := do
-      -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-      -- we don't polute the environment with auxliary declarations.
-      -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
-      -- that modify `CommandElabM` state not just the `Environment`.
-      let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←
-        runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
-          let e ← elabEvalTerm
-          let eType ← instantiateMVars (← inferType e)
-          if eType.isAppOfArity ``CommandElabM 1 then
-            let mut stx ← Term.exprToSyntax e
-            unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
-              stx ← `($stx >>= fun v => IO.println (repr v))
-            let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
-            pure <| Sum.inl act
-          else
-            let e ← mkRunMetaEval e
-            addAndCompile e
-            let act ← evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName
-            pure <| Sum.inr act
-      match act with
-      | .inl act => act
-      | .inr act =>
-        let (out, res) ← act (← getEnv) (← getOptions)
-        logInfoAt tk out
-        match res with
-        | Except.error e => throwError e.toString
-        | Except.ok env  => setEnv env; pure ()
+      -- act? is `some act` if elaborated `term` has type `CommandElabM α`
+      let act? ← runTermElabM fun _ => Term.withDeclName declName do
+        let e ← elabEvalTerm
+        let eType ← instantiateMVars (← inferType e)
+        if eType.isAppOfArity ``CommandElabM 1 then
+          let mut stx ← Term.exprToSyntax e
+          unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
+            stx ← `($stx >>= fun v => IO.println (repr v))
+          let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
+          pure <| some act
+        else
+          let e ← mkRunMetaEval e
+          let env ← getEnv
+          let opts ← getOptions
+          let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
+          let (out, res) ← act env opts -- we execute `act` using the environment
+          logInfoAt tk out
+          match res with
+          | Except.error e => throwError e.toString
+          | Except.ok env  => do setEnv env; pure none
+      let some act := act? | return ()
+      act
     -- Evaluate using term using `Eval` class.
-    let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
+    let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do
       -- fall back to non-meta eval if MetaEval hasn't been defined yet
       -- modify e to `runEval e`
       let e ← mkRunEval (← elabEvalTerm)
-      addAndCompile e
-      let act ← evalConst (IO (String × Except IO.Error Unit)) declName
+      let env ← getEnv
+      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
       let (out, res) ← liftM (m := IO) act
       logInfoAt tk out
       match res with
@@ -704,39 +699,6 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
-private def checkImportsForRunCmds : CommandElabM Unit := do
-  unless (← getEnv).contains ``CommandElabM do
-    throwError "to use this command, include `import Lean.Elab.Command`"
-
-@[builtin_command_elab runCmd]
-def elabRunCmd : CommandElab
-  | `(run_cmd $elems:doSeq) => do
-    checkImportsForRunCmds
-    (← liftTermElabM <| Term.withDeclName `_run_cmd <|
-      unsafe Term.evalTerm (CommandElabM Unit)
-        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(discard do $elems)))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab runElab]
-def elabRunElab : CommandElab
-  | `(run_elab $elems:doSeq) => do
-    checkImportsForRunCmds
-    (← liftTermElabM <| Term.withDeclName `_run_elab <|
-      unsafe Term.evalTerm (CommandElabM Unit)
-        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(Command.liftTermElabM <| discard do $elems)))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab runMeta]
-def elabRunMeta : CommandElab := fun stx =>
-  match stx with
-  | `(run_meta $elems:doSeq) => do
-     checkImportsForRunCmds
-     let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
-     withMacroExpansion stx stxNew do elabCommand stxNew
-  | _ => throwUnsupportedSyntax
-
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
   let term := stx[1]
   withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do

src/Lean/Elab/BuiltinNotation.lean

@@ -7,10 +7,8 @@ import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
 import Lean.Meta.Closure
 import Lean.Meta.MatchUtil
-import Lean.Compiler.ImplementedByAttr
 import Lean.Elab.SyntheticMVars
-import Lean.Elab.Eval
-import Lean.Elab.Binders
+import Lean.Compiler.ImplementedByAttr
 
 namespace Lean.Elab.Term
 open Meta
@@ -429,6 +427,12 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let e ← elabTerm stx[1] expectedType?
   return DiscrTree.mkNoindexAnnotation e
 
+-- TODO: investigate whether we need this function
+private def mkAuxNameForElabUnsafe (hint : Name) : TermElabM Name :=
+  withFreshMacroScope do
+    let name := (← getDeclName?).getD Name.anonymous ++ hint
+    return addMacroScope (← getMainModule) name (← getCurrMacroScope)
+
 @[builtin_term_elab «unsafe»]
 def elabUnsafe : TermElab := fun stx expectedType? =>
   match stx with
@@ -439,7 +443,7 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
     let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
     let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-    let implName ← mkAuxName `unsafe_impl
+    let implName ← mkAuxNameForElabUnsafe `impl
     addDecl <| Declaration.defnDecl {
       name        := implName
       type        := unsafeDefn.type
@@ -452,44 +456,4 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs
   | _ => throwUnsupportedSyntax
 
-/-- Elaborator for `by_elab`. -/
-@[builtin_term_elab byElab] def elabRunElab : TermElab := fun stx expectedType? =>
-  match stx with
-  | `(by_elab $cmds:doSeq) => do
-    if let `(Lean.Parser.Term.doSeq| $e:term) := cmds then
-      if e matches `(Lean.Parser.Term.doSeq| fun $[$_args]* => $_) then
-        let tac ← unsafe evalTerm
-          (Option Expr → TermElabM Expr)
-          (Lean.mkForall `x .default
-            (mkApp (Lean.mkConst ``Option) (Lean.mkConst ``Expr))
-            (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))) e
-        return ← tac expectedType?
-    (← unsafe evalTerm (TermElabM Expr) (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))
-      (← `(do $cmds)))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_term_elab Lean.Parser.Term.haveI] def elabHaveI : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(haveI $x:ident $bs* : $ty := $val; $body) =>
-    withExpectedType expectedType? fun expectedType => do
-      let (ty, val) ← elabBinders bs fun bs => do
-        let ty ← elabType ty
-        let val ← elabTermEnsuringType val ty
-        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-      withLocalDeclD x.getId ty fun x => do
-        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-  | _ => throwUnsupportedSyntax
-
-@[builtin_term_elab Lean.Parser.Term.letI] def elabLetI : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(letI $x:ident $bs* : $ty := $val; $body) =>
-    withExpectedType expectedType? fun expectedType => do
-      let (ty, val) ← elabBinders bs fun bs => do
-        let ty ← elabType ty
-        let val ← elabTermEnsuringType val ty
-        pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-      withLetDecl x.getId ty val fun x => do
-        return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Term

src/Lean/Elab/ElabRules.lean

@@ -11,6 +11,12 @@ open Lean.Syntax
 open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
+def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
+  Term.tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType ← pure expectedType?
+    | throwError "expected type must be known"
+  x expectedType
+
 def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     (attrs? : Option (TSepArray ``attrInstance ",")) (attrKind : TSyntax ``attrKind)
     (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) :
@@ -48,7 +54,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     if catName == `term then
       `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*]
         aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
-        fun stx expectedType? => Lean.Elab.Term.withExpectedType expectedType? fun $expId => match stx with
+        fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
           $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
     else
       throwErrorAt expId "syntax category '{catName}' does not support expected type specification"

src/Lean/Elab/Eval.lean

@@ -9,7 +9,7 @@ import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Term
 open Meta
 
-unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := withoutModifyingEnv do
+unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := do
   let v ← elabTermEnsuringType value type
   synthesizeSyntheticMVarsNoPostponing
   let v ← instantiateMVars v

src/Lean/Elab/Tactic.lean

@@ -26,5 +26,4 @@ import Lean.Elab.Tactic.Congr
 import Lean.Elab.Tactic.Guard
 import Lean.Elab.Tactic.RCases
 import Lean.Elab.Tactic.Repeat
-import Lean.Elab.Tactic.Ext
 import Lean.Elab.Tactic.Change

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -9,11 +9,9 @@ import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
 import Lean.Elab.Binders
 import Lean.Elab.Open
-import Lean.Elab.Eval
 import Lean.Elab.SetOption
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
-import Lean.Elab.Do
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -326,8 +324,11 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 @[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>
   liftMetaTactic fun mvarId => return [← substVars mvarId]
 
-@[builtin_tactic Lean.Parser.Tactic.substEqs] def evalSubstEqs : Tactic := fun _ =>
-  Elab.Tactic.liftMetaTactic1 (·.substEqs)
+/--
+`subst_eq` repeatedly substitutes according to the equality proof hypotheses in the context,
+replacing the left side of the equality with the right, until no more progress can be made.
+-/
+elab "subst_eqs" : tactic => Elab.Tactic.liftMetaTactic1 (·.substEqs)
 
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
@@ -480,25 +481,4 @@ where
 @[builtin_tactic right] def evalRight : Tactic := fun _stx => do
   liftMetaTactic (fun g => g.nthConstructor `right 1 (some 2))
 
-@[builtin_tactic replace] def evalReplace : Tactic := fun stx => do
-  match stx with
-  | `(tactic| replace $decl:haveDecl) =>
-    withMainContext do
-      let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
-      let origLCtx ← getLCtx
-      evalTactic $ ← `(tactic| have $decl:haveDecl)
-      let mut toClear := #[]
-      for fv in vars do
-        if let some ldecl := origLCtx.findFromUserName? fv.getId then
-          toClear := toClear.push ldecl.fvarId
-      liftMetaTactic1 (·.tryClearMany toClear)
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic runTac] def evalRunTac : Tactic := fun stx => do
-  match stx with
-  | `(tactic| run_tac $e:doSeq) =>
-    ← unsafe Term.evalTerm (TacticM Unit) (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Unit))
-      (← `(discard do $e))
-  | _ => throwUnsupportedSyntax
-
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Ext.lean

@@ -1,269 +0,0 @@
-/-
-Copyright (c) 2021 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro
--/
-import Lean.Elab.Tactic.RCases
-import Lean.Elab.Tactic.Repeat
-import Lean.Elab.Tactic.BuiltinTactic
-import Lean.Elab.Command
-import Lean.Linter.Util
-
-namespace Lean.Elab.Tactic.Ext
-open Meta Term
-/-- Information about an extensionality theorem, stored in the environment extension. -/
-structure ExtTheorem where
-  /-- Declaration name of the extensionality theorem. -/
-  declName : Name
-  /-- Priority of the extensionality theorem. -/
-  priority : Nat
-  /--
-  Key in the discrimination tree,
-  for the type in which the extensionality theorem holds.
-  -/
-  keys : Array DiscrTree.Key
-  deriving Inhabited, Repr, BEq, Hashable
-
-/-- The state of the `ext` extension environment -/
-structure ExtTheorems where
-  /-- The tree of `ext` extensions. -/
-  tree   : DiscrTree ExtTheorem := {}
-  /-- Erased `ext`s via `attribute [-ext]`. -/
-  erased  : PHashSet Name := {}
-  deriving Inhabited
-
-/-- Discrimation tree settings for the `ext` extension. -/
-def extExt.config : WhnfCoreConfig := {}
-
-/-- The environment extension to track `@[ext]` theorems. -/
-builtin_initialize extExtension :
-    SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
-  registerSimpleScopedEnvExtension {
-    addEntry := fun { tree, erased } thm =>
-      { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName }
-    initial := {}
-  }
-
-/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`,
-ordered from high priority to low. -/
-@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
-  let extTheorems := extExtension.getState (← getEnv)
-  let arr ← extTheorems.tree.getMatch ty extExt.config
-  let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
-  -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
-  -- Most ext theorems have default priority.
-  return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse
-
-/--
-Erases a name marked `ext` by adding it to the state's `erased` field and
-removing it from the state's list of `Entry`s.
-
-This is triggered by `attribute [-ext] name`.
--/
-def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems :=
- { d with erased := d.erased.insert declName }
-
-/--
-  Erases a name marked as a `ext` attribute.
-  Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem`
-  found somewhere in the state's tree, and is not erased.
--/
-def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
-    m ExtTheorems := do
-  unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do
-    throwError "'{declName}' does not have [ext] attribute"
-  return d.eraseCore declName
-
-builtin_initialize registerBuiltinAttribute {
-  name := `ext
-  descr := "Marks a theorem as an extensionality theorem"
-  add := fun declName stx kind => do
-    let `(attr| ext $[(flat := $f)]? $(prio)?) := stx
-      | throwError "unexpected @[ext] attribute {stx}"
-    if isStructure (← getEnv) declName then
-      liftCommandElabM <| Elab.Command.elabCommand <|
-        ← `(declare_ext_theorems_for $[(flat := $f)]? $(mkCIdentFrom stx declName) $[$prio]?)
-    else MetaM.run' do
-      if let some flat := f then
-        throwErrorAt flat "unexpected 'flat' config on @[ext] theorem"
-      let declTy := (← getConstInfo declName).type
-      let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing declTy
-      let failNotEq := throwError
-        "@[ext] attribute only applies to structures or theorems proving x = y, got {declTy}"
-      let some (ty, lhs, rhs) := declTy.eq? | failNotEq
-      unless lhs.isMVar && rhs.isMVar do failNotEq
-      let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
-      let priority ← liftCommandElabM do Elab.liftMacroM do
-        evalPrio (prio.getD (← `(prio| default)))
-      extExtension.add {declName, keys, priority} kind
-  erase := fun declName => do
-    let s := extExtension.getState (← getEnv)
-    let s ← s.erase declName
-    modifyEnv fun env => extExtension.modifyState env fun _ => s
-}
-
-/--
-Constructs the hypotheses for the structure extensionality theorem that
-states that two structures are equal if their fields are equal.
-
-Calls the continuation `k` with the list of parameters to the structure,
-two structure variables `x` and `y`, and a list of pairs `(field, ty)`
-where `ty` is `x.field = y.field` or `HEq x.field y.field`.
-
-If `flat` parses to `true`, any fields inherited from parent structures
-are treated fields of the given structure type.
-If it is `false`, then the behind-the-scenes encoding of inherited fields
-is visible in the extensionality lemma.
--/
--- TODO: this is probably the wrong place to have this function
-def withExtHyps (struct : Name) (flat : Term)
-    (k : Array Expr → (x y : Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
-  let flat ← match flat with
-  | `(true) => pure true
-  | `(false) => pure false
-  | _ => throwErrorAt flat "expected 'true' or 'false'"
-  unless isStructure (← getEnv) struct do throwError "not a structure: {struct}"
-  let structC ← mkConstWithLevelParams struct
-  forallTelescope (← inferType structC) fun params _ => do
-  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
-  withLocalDeclD `x (mkAppN structC params) fun x => do
-  withLocalDeclD `y (mkAppN structC params) fun y => do
-    let mut hyps := #[]
-    let fields := if flat then
-      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
-    else
-      getStructureFields (← getEnv) struct
-    for field in fields do
-      let x_f ← mkProjection x field
-      let y_f ← mkProjection y field
-      if ← isProof x_f then
-        pure ()
-      else if ← isDefEq (← inferType x_f) (← inferType y_f) then
-        hyps := hyps.push (field, ← mkEq x_f y_f)
-      else
-        hyps := hyps.push (field, ← mkHEq x_f y_f)
-    k params x y hyps
-
-/--
-Creates the type of the extensionality theorem for the given structure,
-elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
--/
-@[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
-  match stx with
-  | `(ext_type%  $flat:term $struct:ident) => do
-    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
-      let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
-        mkForall f BinderInfo.default h ty
-      mkForallFVars (params |>.push x |>.push y) ty
-  | _ => throwUnsupportedSyntax
-
-/--
-Creates the type of the iff-variant of the extensionality theorem for the given structure,
-elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
--/
-@[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
-  match stx with
-  | `(ext_iff_type% $flat:term $struct:ident) => do
-    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
-      mkForallFVars (params |>.push x |>.push y) <|
-        mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
-  | _ => throwUnsupportedSyntax
-
-/-- Apply a single extensionality theorem to `goal`. -/
-def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do
-  let tgt ← goal.getType'
-  unless tgt.isAppOfArity ``Eq 3 do
-    throwError "applyExtTheorem only applies to equations, not{indentExpr tgt}"
-  let ty := tgt.getArg! 0
-  let s ← saveState
-  for lem in ← getExtTheorems ty do
-    try
-      -- Note: We have to do this extra check to ensure that we don't apply e.g.
-      -- funext to a goal `(?a₁ : ?b) = ?a₂` to produce `(?a₁ x : ?b') = ?a₂ x`,
-      -- since this will loop.
-      -- We require that the type of the equality is not changed by the `goal.apply c` line
-      -- TODO: add flag to apply tactic to toggle unification vs. matching
-      withNewMCtxDepth do
-        let c ← mkConstWithFreshMVarLevels lem.declName
-        let (_, _, declTy) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
-        guard (← isDefEq tgt declTy)
-      -- We use `newGoals := .all` as this is
-      -- more useful in practice with dependently typed arguments of `@[ext]` theorems.
-      return ← goal.apply (cfg := { newGoals := .all }) (← mkConstWithFreshMVarLevels lem.declName)
-    catch _ => s.restore
-  throwError "no applicable extensionality theorem found for{indentExpr ty}"
-
-/-- Apply a single extensionality theorem to the current goal. -/
-@[builtin_tactic applyExtTheorem] def evalApplyExtTheorem : Tactic := fun _ => do
-  liftMetaTactic applyExtTheoremAt
-
-/--
-Postprocessor for `withExt` which runs `rintro` with the given patterns when the target is a
-pi type.
--/
-def tryIntros [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
-    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
-  match pats with
-  | [] => k (← (g.intros : TermElabM _)).2 []
-  | p::ps =>
-    if (← (g.withContext g.getType' : TermElabM _)).isForall then
-      let mut n := 0
-      for g in ← RCases.rintro #[p] none g do
-        n := n.max (← tryIntros g ps k)
-      pure (n + 1)
-    else k g pats
-
-/--
-Applies a single extensionality theorem, using `pats` to introduce variables in the result.
-Runs continuation `k` on each subgoal.
--/
-def withExt1 [Monad m] [MonadLiftT TermElabM m] (g : MVarId) (pats : List (TSyntax `rcasesPat))
-    (k : MVarId → List (TSyntax `rcasesPat) → m Nat) : m Nat := do
-  let mut n := 0
-  for g in ← (applyExtTheoremAt g : TermElabM _) do
-    n := n.max (← tryIntros g pats k)
-  pure n
-
-/--
-Applies extensionality theorems recursively, using `pats` to introduce variables in the result.
-Runs continuation `k` on each subgoal.
--/
-def withExtN [Monad m] [MonadLiftT TermElabM m] [MonadExcept Exception m]
-    (g : MVarId) (pats : List (TSyntax `rcasesPat)) (k : MVarId → List (TSyntax `rcasesPat) → m Nat)
-    (depth := 1000000) (failIfUnchanged := true) : m Nat :=
-  match depth with
-  | 0 => k g pats
-  | depth+1 => do
-    if failIfUnchanged then
-      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
-    else try
-      withExt1 g pats fun g pats => withExtN g pats k depth (failIfUnchanged := false)
-    catch _ => k g pats
-
-/--
-Apply extensionality theorems as much as possible, using `pats` to introduce the variables
-in extensionality theorems like `funext`. Returns a list of subgoals.
-
-This is built on top of `withExtN`, running in `TermElabM` to build the list of new subgoals.
-(And, for each goal, the patterns consumed.)
--/
-def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
-    (depth := 1000000) (failIfUnchanged := true) :
-    TermElabM (Nat × Array (MVarId × List (TSyntax `rcasesPat))) := do
-  StateT.run (m := TermElabM) (s := #[])
-    (withExtN g pats (fun g qs => modify (·.push (g, qs)) *> pure 0) depth failIfUnchanged)
-
-@[builtin_tactic ext] def evalExt : Tactic := fun stx => do
-  match stx with
-  | `(tactic| ext $pats* $[: $n]?) => do
-    let pats := RCases.expandRIntroPats pats
-    let depth := n.map (·.getNat) |>.getD 1000000
-    let (used, gs) ← extCore (← getMainGoal) pats.toList depth
-    if RCases.linter.unusedRCasesPattern.get (← getOptions) then
-      if used < pats.size then
-        Linter.logLint RCases.linter.unusedRCasesPattern (mkNullNode pats[used:].toArray)
-          m!"`ext` did not consume the patterns: {pats[used:]}"
-    replaceMainGoal <| gs.map (·.1) |>.toList
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.Ext

src/Lean/Elab/Term.lean

@@ -865,12 +865,6 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla
     throwError "{msg}, expected type contains metavariables{indentD expectedType?}"
   return expectedType
 
-def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
-  tryPostponeIfNoneOrMVar expectedType?
-  let some expectedType ← pure expectedType?
-    | throwError "expected type must be known"
-  x expectedType
-
 /--
   Save relevant context for term elaboration postponement.
 -/

src/Lean/Expr.lean

@@ -1916,14 +1916,7 @@ def mkNot (p : Expr) : Expr := mkApp (mkConst ``Not) p
 def mkOr (p q : Expr) : Expr := mkApp2 (mkConst ``Or) p q
 /-- Return `p ∧ q` -/
 def mkAnd (p q : Expr) : Expr := mkApp2 (mkConst ``And) p q
-/-- Make an n-ary `And` application. `mkAndN []` returns `True`. -/
-def mkAndN : List Expr → Expr
-  | [] => mkConst ``True
-  | [p] => p
-  | p :: ps => mkAnd p (mkAndN ps)
 /-- Return `Classical.em p` -/
 def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
-/-- Return `p ↔ q` -/
-def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
 end Lean

src/Lean/Meta/Tactic.lean

@@ -22,7 +22,6 @@ import Lean.Meta.Tactic.Simp
 import Lean.Meta.Tactic.AuxLemma
 import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.Split
-import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Tactic.Rename

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -12,13 +12,9 @@ import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 namespace Lean.Meta
 namespace Simp
 
-/-- The result of simplifying some expression `e`. -/
 structure Result where
-  /-- The simplified version of `e` -/ 
   expr           : Expr
-  /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
-  If `none`, the proof is assumed to be `refl`. -/
-  proof?         : Option Expr := none
+  proof?         : Option Expr := none -- If none, proof is assumed to be `refl`
   /-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
   dischargeDepth : UInt32 := 0
   /-- If `cache := true` the result is cached. -/

src/Lean/Meta/Tactic/TryThis.lean

@@ -1,585 +0,0 @@
-/-
-Copyright (c) 2021 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Mario Carneiro, Thomas Murrills
--/
-import Lean.Server.CodeActions
-import Lean.Widget.UserWidget
-import Lean.Data.Json.Elab
-
-/-- Gets the LSP range from a `String.Range`. -/
-def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
-
-/-!
-# "Try this" support
-
-This implements a mechanism for tactics to print a message saying `Try this: <suggestion>`,
-where `<suggestion>` is a link to a replacement tactic. Users can either click on the link
-in the suggestion (provided by a widget), or use a code action which applies the suggestion.
--/
-namespace Lean.Meta.Tactic.TryThis
-
-open Lean Elab PrettyPrinter Meta Server RequestM
-
-/-! # Raw widget -/
-
-/--
-This is a widget which is placed by `TryThis.addSuggestion` and `TryThis.addSuggestions`.
-
-When placed by `addSuggestion`, it says `Try this: <replacement>`
-where `<replacement>` is a link which will perform the replacement.
-
-When placed by `addSuggestions`, it says:
-```
-Try these:
-```
-* `<replacement1>`
-* `<replacement2>`
-* `<replacement3>`
-* ...
-
-where `<replacement*>` is a link which will perform the replacement.
--/
-@[widget_module] def tryThisWidget : Widget.Module where
-  javascript := "
-import * as React from 'react';
-import { EditorContext } from '@leanprover/infoview';
-const e = React.createElement;
-export default function ({ pos, suggestions, range, header, isInline, style }) {
-  const editorConnection = React.useContext(EditorContext)
-  const defStyle = style || {
-    className: 'link pointer dim',
-    style: { color: 'var(--vscode-textLink-foreground)' }
-  }
-
-  // Construct the children of the HTML element for a given suggestion.
-  function makeSuggestion({ suggestion, preInfo, postInfo, style }) {
-    function onClick() {
-      editorConnection.api.applyEdit({
-        changes: { [pos.uri]: [{ range, newText: suggestion }] }
-      })
-    }
-    return [
-      preInfo,
-      e('span', { onClick, title: 'Apply suggestion', ...style || defStyle }, suggestion),
-      postInfo
-    ]
-  }
-
-  // Choose between an inline 'Try this'-like display and a list-based 'Try these'-like display.
-  let inner = null
-  if (isInline) {
-    inner = e('div', { className: 'ml1' },
-      e('pre', { className: 'font-code pre-wrap' }, header, makeSuggestion(suggestions[0])))
-  } else {
-    inner = e('div', { className: 'ml1' },
-      e('pre', { className: 'font-code pre-wrap' }, header),
-      e('ul', { style: { paddingInlineStart: '20px' } }, suggestions.map(s =>
-        e('li', { className: 'font-code pre-wrap' }, makeSuggestion(s)))))
-  }
-  return e('details', { open: true },
-    e('summary', { className: 'mv2 pointer' }, 'Suggestions'),
-    inner)
-}"
-
-/-! # Code action -/
-
-/-- A packet of information about a "Try this" suggestion
-that we store in the infotree for the associated code action to retrieve. -/
-structure TryThisInfo : Type where
-  /-- The textual range to be replaced by one of the suggestions. -/
-  range : Lsp.Range
-  /--
-  A list of suggestions for the user to choose from.
-  Each suggestion may optionally come with an override for the code action title.
-  -/
-  suggestionTexts : Array (String × Option String)
-  /-- The prefix to display before the code action for a "Try this" suggestion if no custom code
-  action title is provided. If not provided, `"Try this: "` is used. -/
-  codeActionPrefix? : Option String
-  deriving TypeName
-
-/--
-This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
-apply the replacement.
--/
-@[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do
-  let doc ← readDoc
-  pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
-    let .ofCustomInfo { stx, value } := info | result
-    let some { range, suggestionTexts, codeActionPrefix? } :=
-      value.get? TryThisInfo | result
-    let some stxRange := stx.getRange? | result
-    let stxRange := doc.meta.text.utf8RangeToLspRange stxRange
-    unless stxRange.start.line ≤ params.range.end.line do return result
-    unless params.range.start.line ≤ stxRange.end.line do return result
-    let mut result := result
-    for h : i in [:suggestionTexts.size] do
-      let (newText, title?) := suggestionTexts[i]'h.2
-      let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
-      result := result.push {
-        eager.title := title
-        eager.kind? := "quickfix"
-        -- Only make the first option preferred
-        eager.isPreferred? := if i = 0 then true else none
-        eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText }
-      }
-    result
-
-/-! # Formatting -/
-
-/-- Yields `(indent, column)` given a `FileMap` and a `String.Range`, where `indent` is the number
-of spaces by which the line that first includes `range` is initially indented, and `column` is the
-column `range` starts at in that line. -/
-def getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat :=
-  let start := map.source.findLineStart range.start
-  let body := map.source.findAux (· ≠ ' ') range.start start
-  ((body - start).1, (range.start - start).1)
-
-/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/
-partial def replaceMVarsByUnderscores [Monad m] [MonadQuotation m]
-    (s : Syntax) : m Syntax :=
-  s.replaceM fun s => do
-    let `(?$id:ident) := s | pure none
-    if id.getId.hasNum || id.getId.isInternal then `(?_) else pure none
-
-/-- Delaborate `e` into syntax suitable for use by `refine`. -/
-def delabToRefinableSyntax (e : Expr) : MetaM Term :=
-  return ⟨← replaceMVarsByUnderscores (← delab e)⟩
-
-/--
-An option allowing the user to customize the ideal input width. Defaults to 100.
-This option controls output format when
-the output is intended to be copied back into a lean file -/
-register_option format.inputWidth : Nat := {
-  /- The default maximum width of an ideal line in source code. -/
-  defValue := 100
-  descr := "ideal input width"
-}
-
-/-- Get the input width specified in the options -/
-def getInputWidth (o : Options) : Nat := format.inputWidth.get o
-
-/-! # `Suggestion` data -/
-
--- TODO: we could also support `Syntax` and `Format`
-/-- Text to be used as a suggested replacement in the infoview. This can be either a `TSyntax kind`
-for a single `kind : SyntaxNodeKind` or a raw `String`.
-
-Instead of using constructors directly, there are coercions available from these types to
-`SuggestionText`. -/
-inductive SuggestionText where
-  /-- `TSyntax kind` used as suggested replacement text in the infoview. Note that while `TSyntax`
-  is in general parameterized by a list of `SyntaxNodeKind`s, we only allow one here; this
-  unambiguously guides pretty-printing. -/
-  | tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText
-  /-- A raw string to be used as suggested replacement text in the infoview. -/
-  | string : String → SuggestionText
-  deriving Inhabited
-
-instance : ToMessageData SuggestionText where
-  toMessageData
-  | .tsyntax stx => stx
-  | .string s => s
-
-instance {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText where
-  coe := .tsyntax
-
-instance : Coe String SuggestionText where
-  coe := .string
-
-namespace SuggestionText
-
-/-- Pretty-prints a `SuggestionText` as a `Format`. If the `SuggestionText` is some `TSyntax kind`,
-we use the appropriate pretty-printer; strings are coerced to `Format`s as-is. -/
-def pretty : SuggestionText → CoreM Format
-  | .tsyntax (kind := kind) stx => ppCategory kind stx
-  | .string text => return text
-
-/- Note that this is essentially `return (← s.pretty).prettyExtra w indent column`, but we
-special-case strings to avoid converting them to `Format`s and back, which adds indentation after each newline. -/
-/-- Pretty-prints a `SuggestionText` as a `String` and wraps with respect to the pane width,
-indentation, and column, via `Format.prettyExtra`. If `w := none`, then
-`w := getInputWidth (← getOptions)` is used. Raw `String`s are returned as-is. -/
-def prettyExtra (s : SuggestionText) (w : Option Nat := none)
-    (indent column : Nat := 0) : CoreM String :=
-  match s with
-  | .tsyntax (kind := kind) stx => do
-    let w ← match w with | none => do pure <| getInputWidth (← getOptions) | some n => pure n
-    return (← ppCategory kind stx).pretty w indent column
-  | .string text => return text
-
-end SuggestionText
-
-/--
-Style hooks for `Suggestion`s. See `SuggestionStyle.error`, `.warning`, `.success`, `.value`,
-and other definitions here for style presets. This is an arbitrary `Json` object, with the following
-interesting fields:
-* `title`: the hover text in the suggestion link
-* `className`: the CSS classes applied to the link
-* `style`: A `Json` object with additional inline CSS styles such as `color` or `textDecoration`.
--/
-def SuggestionStyle := Json deriving Inhabited, ToJson
-
-/-- Style as an error. By default, decorates the text with an undersquiggle; providing the argument
-`decorated := false` turns this off. -/
-def SuggestionStyle.error (decorated := true) : SuggestionStyle :=
-  let style := if decorated then
-    json% {
-      -- The VS code error foreground theme color (`--vscode-errorForeground`).
-      color: "var(--vscode-errorForeground)",
-      textDecoration: "underline wavy var(--vscode-editorError-foreground) 1pt"
-    }
-  else json% { color: "var(--vscode-errorForeground)" }
-  json% { className: "pointer dim", style: $style }
-
-/-- Style as a warning. By default, decorates the text with an undersquiggle; providing the
-argument `decorated := false` turns this off. -/
-def SuggestionStyle.warning (decorated := true) : SuggestionStyle :=
-  if decorated then
-    json% {
-      -- The `.gold` CSS class, which the infoview uses when e.g. building a file.
-      className: "gold pointer dim",
-      style: { textDecoration: "underline wavy var(--vscode-editorWarning-foreground) 1pt" }
-    }
-  else json% { className: "gold pointer dim" }
-
-/-- Style as a success. -/
-def SuggestionStyle.success : SuggestionStyle :=
-  -- The `.information` CSS class, which the infoview uses on successes.
-  json% { className: "information pointer dim" }
-
-/-- Style the same way as a hypothesis appearing in the infoview. -/
-def SuggestionStyle.asHypothesis : SuggestionStyle :=
-  json% { className: "goal-hyp pointer dim" }
-
-/-- Style the same way as an inaccessible hypothesis appearing in the infoview. -/
-def SuggestionStyle.asInaccessible : SuggestionStyle :=
-  json% { className: "goal-inaccessible pointer dim" }
-
-/-- Draws the color from a red-yellow-green color gradient with red at `0.0`, yellow at `0.5`, and
-green at `1.0`. Values outside the range `[0.0, 1.0]` are clipped to lie within this range.
-
-With `showValueInHoverText := true` (the default), the value `t` will be included in the `title` of
-the HTML element (which appears on hover). -/
-def SuggestionStyle.value (t : Float) (showValueInHoverText := true) : SuggestionStyle :=
-  let t := min (max t 0) 1
-  json% {
-    className: "pointer dim",
-    -- interpolates linearly from 0º to 120º with 95% saturation and lightness
-    -- varying around 50% in HSL space
-    style: { color: $(s!"hsl({(t * 120).round} 95% {60 * ((t - 0.5)^2 + 0.75)}%)") },
-    title: $(if showValueInHoverText then s!"Apply suggestion ({t})" else "Apply suggestion")
-  }
-
-/-- Holds a `suggestion` for replacement, along with `preInfo` and `postInfo` strings to be printed
-immediately before and after that suggestion, respectively. It also includes an optional
-`MessageData` to represent the suggestion in logs; by default, this is `none`, and `suggestion` is
-used. -/
-structure Suggestion where
-  /-- Text to be used as a replacement via a code action. -/
-  suggestion : SuggestionText
-  /-- Optional info to be printed immediately before replacement text in a widget. -/
-  preInfo? : Option String := none
-  /-- Optional info to be printed immediately after replacement text in a widget. -/
-  postInfo? : Option String := none
-  /-- Optional style specification for the suggestion. If `none` (the default), the suggestion is
-  styled as a text link. Otherwise, the suggestion can be styled as:
-  * a status: `.error`, `.warning`, `.success`
-  * a hypothesis name: `.asHypothesis`, `.asInaccessible`
-  * a variable color: `.value (t : Float)`, which draws from a red-yellow-green gradient, with red
-  at `0.0` and green at `1.0`.
-
-  See `SuggestionStyle` for details. -/
-  style? : Option SuggestionStyle := none
-  /-- How to represent the suggestion as `MessageData`. This is used only in the info diagnostic.
-  If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner. -/
-  messageData? : Option MessageData := none
-  /-- How to construct the text that appears in the lightbulb menu from the suggestion text. If
-  `none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed
-  `suggestion : SuggestionText` is used here. -/
-  toCodeActionTitle? : Option (String → String) := none
-  deriving Inhabited
-
-/-- Converts a `Suggestion` to `Json` in `CoreM`. We need `CoreM` in order to pretty-print syntax.
-
-This also returns a `String × Option String` consisting of the pretty-printed text and any custom
-code action title if `toCodeActionTitle?` is provided.
-
-If `w := none`, then `w := getInputWidth (← getOptions)` is used.
--/
-def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
-    CoreM (Json × String × Option String) := do
-  let text ← s.suggestion.prettyExtra w indent column
-  let mut json := [("suggestion", (text : Json))]
-  if let some preInfo := s.preInfo? then json := ("preInfo", preInfo) :: json
-  if let some postInfo := s.postInfo? then json := ("postInfo", postInfo) :: json
-  if let some style := s.style? then json := ("style", toJson style) :: json
-  return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text))
-
-/- If `messageData?` is specified, we use that; otherwise (by default), we use `toMessageData` of
-the suggestion text. -/
-instance : ToMessageData Suggestion where
-  toMessageData s := s.messageData?.getD (toMessageData s.suggestion)
-
-instance : Coe SuggestionText Suggestion where
-  coe t := { suggestion := t }
-
-/-- Delaborate `e` into a suggestion suitable for use by `refine`. -/
-def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
-  return { suggestion := ← delabToRefinableSyntax e, messageData? := e }
-
-/-! # Widget hooks -/
-
-/-- Core of `addSuggestion` and `addSuggestions`. Whether we use an inline display for a single
-element or a list display is controlled by `isInline`. -/
-private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion)
-    (header : String) (isInline : Bool) (origSpan? : Option Syntax := none)
-    (style? : Option SuggestionStyle := none)
-    (codeActionPrefix? : Option String := none) : CoreM Unit := do
-  if let some range := (origSpan?.getD ref).getRange? then
-    let map ← getFileMap
-    -- FIXME: this produces incorrect results when `by` is at the beginning of the line, i.e.
-    -- replacing `tac` in `by tac`, because the next line will only be 2 space indented
-    -- (less than `tac` which starts at column 3)
-    let (indent, column) := getIndentAndColumn map range
-    let suggestions ← suggestions.mapM (·.toJsonAndInfoM (indent := indent) (column := column))
-    let suggestionTexts := suggestions.map (·.2)
-    let suggestions := suggestions.map (·.1)
-    let ref := Syntax.ofRange <| ref.getRange?.getD range
-    let range := map.utf8RangeToLspRange range
-    pushInfoLeaf <| .ofCustomInfo {
-      stx := ref
-      value := Dynamic.mk
-        { range, suggestionTexts, codeActionPrefix? : TryThisInfo }
-    }
-    Widget.savePanelWidgetInfo (hash tryThisWidget.javascript) ref
-      (props := return json% {
-        suggestions: $suggestions,
-        range: $range,
-        header: $header,
-        isInline: $isInline,
-        style: $style?
-      })
-
-/-- Add a "try this" suggestion. This has three effects:
-
-* An info diagnostic is displayed saying `Try this: <suggestion>`
-* A widget is registered, saying `Try this: <suggestion>` with a link on `<suggestion>` to apply
-  the suggestion
-* A code action is added, which will apply the suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `s`: a `Suggestion`, which contains
-  * `suggestion`: the replacement text;
-  * `preInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `style?`: an optional `Json` object used as the value of the `style` attribute of the
-    suggestion text's element (not the whole suggestion element).
-  * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
-    (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
-    `suggestion` instead.
-  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
-    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
-    If `none`, we simply prepend `"Try This: "` to the suggestion text.
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string that begins the display. By default, it is `"Try this: "`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none)
-    (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  logInfoAt ref m!"{header}{s}"
-  addSuggestionCore ref #[s] header (isInline := true) origSpan?
-    (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects:
-
-* An info diagnostic is displayed saying `Try these: <list of suggestions>`
-* A widget is registered, saying `Try these: <list of suggestions>` with a link on each
-  `<suggestion>` to apply the suggestion
-* A code action for each suggestion is added, which will apply the suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `suggestions`: an array of `Suggestion`s, which each contain
-  * `suggestion`: the replacement text;
-  * `preInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `postInfo?`: an optional string shown immediately after the replacement text in the widget
-    message (only)
-  * `style?`: an optional `Json` object used as the value of the `style` attribute of the
-    suggestion text's element (not the whole suggestion element).
-  * `messageData?`: an optional message to display in place of `suggestion` in the info diagnostic
-    (only). The widget message uses only `suggestion`. If `messageData?` is `none`, we simply use
-    `suggestion` instead.
-  * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
-    pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
-    If `none`, we simply prepend `"Try This: "` to the suggestion text.
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string that precedes the list. By default, it is `"Try these:"`.
-* `style?`: a default style for all suggestions which do not have a custom `style?` set.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
-    (origSpan? : Option Syntax := none) (header : String := "Try these:")
-    (style? : Option SuggestionStyle := none)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  if suggestions.isEmpty then throwErrorAt ref "no suggestions available"
-  let msgs := suggestions.map toMessageData
-  let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)
-  logInfoAt ref m!"{header}{msgs}"
-  addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
-
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
-  let stx ← delabToRefinableSyntax e
-  let mvars ← getMVars e
-  let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
-  let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
-    let mut str := "\nRemaining subgoals:"
-    for g in mvars do
-      -- TODO: use a MessageData.ofExpr instead of rendering to string
-      let e ← PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
-      str := str ++ Format.pretty ("\n⊢ " ++ e)
-    pure str
-  pure { suggestion, postInfo?, messageData? }
-
-/-- Add an `exact e` or `refine e` suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `e`: the replacement expression
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
-  `Remaining subgoals:`
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addExactSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none): MetaM Unit := do
-  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
-    (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add `exact e` or `refine e` suggestions.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `es`: the array of replacement expressions
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
-  `Remaining subgoals:`
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addExactSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
-  addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add a term suggestion.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `e`: the replacement expression
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string which precedes the suggestion. By default, it's `"Try this: "`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
-  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
--/
-def addTermSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try this: ")
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  addSuggestion ref (← delabToRefinableSuggestion e) (origSpan? := origSpan?) (header := header)
-    (codeActionPrefix? := codeActionPrefix?)
-
-/-- Add term suggestions.
-
-The parameters are:
-* `ref`: the span of the info diagnostic
-* `es`: an array of the replacement expressions
-* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
-  If not provided it defaults to `ref`.
-* `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`.
-* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
-  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
-  used.
--/
-def addTermSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try these:")
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  addSuggestions ref (← es.mapM delabToRefinableSuggestion)
-    (origSpan? := origSpan?) (header := header) (codeActionPrefix? := codeActionPrefix?)
-
-open Lean Elab Elab.Tactic PrettyPrinter Meta
-
-/-- Add a suggestion for `have h : t := e`. -/
-def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e : Expr)
-    (origSpan? : Option Syntax := none) : TermElabM Unit := do
-  let estx ← delabToRefinableSyntax e
-  let prop ← isProp (← inferType e)
-  let tac ← if let some t := t? then
-    let tstx ← delabToRefinableSyntax t
-    if prop then
-      match h? with
-      | some h => `(tactic| have $(mkIdent h) : $tstx := $estx)
-      | none => `(tactic| have : $tstx := $estx)
-    else
-      `(tactic| let $(mkIdent (h?.getD `_)) : $tstx := $estx)
-  else
-    if prop then
-      match h? with
-      | some h => `(tactic| have $(mkIdent h) := $estx)
-      | none => `(tactic| have := $estx)
-    else
-      `(tactic| let $(mkIdent (h?.getD `_)) := $estx)
-  addSuggestion ref tac origSpan?
-
-open Lean.Parser.Tactic
-open Lean.Syntax
-
-/-- Add a suggestion for `rw [h₁, ← h₂] at loc`. -/
-def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
-  (type? : Option Expr := none) (loc? : Option Expr := none)
-  (origSpan? : Option Syntax := none) :
-    TermElabM Unit := do
-  let rules_stx := TSepArray.ofElems <| ← rules.toArray.mapM fun ⟨e, symm⟩ => do
-    let t ← delabToRefinableSyntax e
-    if symm then `(rwRule| ← $t:term) else `(rwRule| $t:term)
-  let tac ← do
-    let loc ← loc?.mapM fun loc => do `(location| at $(← delab loc):term)
-    `(tactic| rw [$rules_stx,*] $(loc)?)
-
-  -- We don't simply write `let mut tacMsg := m!"{tac}"` here
-  -- but instead rebuild it, so that there are embedded `Expr`s in the message,
-  -- thus giving more information in the hovers.
-  -- Perhaps in future we will have a better way to attach elaboration information to
-  -- `Syntax` embedded in a `MessageData`.
-  let mut tacMsg :=
-    let rulesMsg := MessageData.sbracket <| MessageData.joinSep
-      (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", "
-    if let some loc := loc? then
-      m!"rw {rulesMsg} at {loc}"
-    else
-      m!"rw {rulesMsg}"
-  let mut extraMsg := ""
-  if let some type := type? then
-    tacMsg := tacMsg ++ m!"\n-- {type}"
-    extraMsg := extraMsg ++ s!"\n-- {← PrettyPrinter.ppExpr type}"
-  addSuggestion ref (s := { suggestion := tac, postInfo? := extraMsg, messageData? := tacMsg })
-    origSpan?

src/Lean/Parser/Syntax.lean

@@ -104,16 +104,6 @@ def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ide
   optional docComment >> optional Term.«attributes» >> Term.attrKind >>
   "elab" >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> elabArg) >> elabTail
 
-/--
-Declares a binder predicate.  For example:
-```
-binder_predicate x " > " y:term => `($x > $y)
-```
--/
-@[builtin_command_parser] def binderPredicate := leading_parser
-   optional docComment >>  optional Term.attributes >> optional Term.attrKind >>
-   "binder_predicate" >> optNamedName >> optNamedPrio >> ppSpace >> ident >> many (ppSpace >> macroArg) >> " => " >> termParser
-
 end Command
 
 end Parser

src/Lean/Parser/Term.lean

@@ -569,12 +569,6 @@ def haveDecl     := leading_parser (withAnonymousAntiquot := false)
   haveIdDecl <|> (ppSpace >> letPatDecl) <|> haveEqnsDecl
 @[builtin_term_parser] def «have» := leading_parser:leadPrec
   withPosition ("have" >> haveDecl) >> optSemicolon termParser
-/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-@[builtin_term_parser] def «haveI» := leading_parser
-  withPosition ("haveI " >> haveDecl) >> optSemicolon termParser
-/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-@[builtin_term_parser] def «letI» := leading_parser
-  withPosition ("letI " >> haveDecl) >> optSemicolon termParser
 
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -793,50 +793,23 @@ def delabProj : Delab := do
   let idx := Syntax.mkLit fieldIdxKind (toString (idx + 1));
   `($(e).$idx:fieldIdx)
 
-/--
-Delaborates an application of a projection function, for example `Prod.fst p` as `p.fst`.
-Collapses intermediate parent projections, so for example rather than `o.toB.toA.x` it produces `o.x`.
-
-Does not delaborate projection functions from classes, since the instance parameter is implicit;
-we would rather see `default` than `instInhabitedNat.default`.
--/
+/-- Delaborate a call to a projection function such as `Prod.fst`. -/
 @[builtin_delab app]
-partial def delabProjectionApp : Delab := whenPPOption getPPStructureProjections do
-  let (field, arity, _) ← projInfo
-  withOverApp arity do
-    let stx ← withAppArg <| withoutParentProjections delab
-    `($(stx).$(mkIdent field):ident)
-where
-  /--
-  If this is a projection that could delaborate using dot notation,
-  returns the field name, the arity of the projector, and whether this is a parent projection.
-  Otherwise it fails.
-  -/
-  projInfo : DelabM (Name × Nat × Bool) := do
-    let .app fn _ ← getExpr | failure
-    let .const c@(.str _ field) _ := fn.getAppFn | failure
-    let env ← getEnv
-    let some info := env.getProjectionFnInfo? c | failure
-    -- Don't delaborate for classes since the instance parameter is implicit.
-    guard <| !info.fromClass
-    -- If pp.explicit is true, and the structure has parameters, we should not
-    -- use field notation because we will not be able to see the parameters.
-    guard <| !(← getPPOption getPPExplicit) || info.numParams == 0
-    let arity := info.numParams + 1
-    let some (.ctorInfo cVal) := env.find? info.ctorName | failure
-    let isParentProj := (isSubobjectField? env cVal.induct field).isSome
-    return (field, arity, isParentProj)
-  /--
-  Consumes projections to parent structures.
-  For example, if the current expression is `o.toB.toA`, runs `d` with `o` as the current expression.
-  -/
-  withoutParentProjections {α} (d : DelabM α) : DelabM α :=
-    (do
-      let (_, arity, isParentProj) ← projInfo
-      guard isParentProj
-      guard <| (← getExpr).getAppNumArgs == arity
-      withAppArg <| withoutParentProjections d)
-    <|> d
+def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
+  let Expr.app fn _ ← getExpr | failure
+  let .const c@(.str _ f) _ ← pure fn.getAppFn | failure
+  let env ← getEnv
+  let some info ← pure $ env.getProjectionFnInfo? c | failure
+  -- can't use with classes since the instance parameter is implicit
+  guard $ !info.fromClass
+  -- If pp.explicit is true, and the structure has parameters, we should not
+  -- use field notation because we will not be able to see the parameters.
+  let expl ← getPPOption getPPExplicit
+  guard $ !expl || info.numParams == 0
+  -- projection function should be fully applied (#struct params + 1 instance parameter)
+  withOverApp (info.numParams + 1) do
+    let appStx ← withAppArg delab
+    `($(appStx).$(mkIdent f):ident)
 
 /--
 This delaborator tries to elide functions which are known coercions.

src/library/compiler/llvm.cpp

@@ -18,7 +18,6 @@ Lean's IR.
 #include "runtime/string_ref.h"
 
 #ifdef LEAN_LLVM
-#include "llvm-c/Analysis.h"
 #include "llvm-c/BitReader.h"
 #include "llvm-c/BitWriter.h"
 #include "llvm-c/Core.h"
@@ -1425,74 +1424,3 @@ extern "C" LEAN_EXPORT lean_object *llvm_is_declaration(size_t ctx, size_t globa
 	return lean_io_result_mk_ok(lean_box(is_bool));
 #endif  // LEAN_LLVM
 }
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_verify_module(size_t ctx, size_t mod,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    char* msg = NULL;
-    LLVMBool broken = LLVMVerifyModule(lean_to_Module(mod), LLVMReturnStatusAction, &msg);
-    if (broken) {
-      return lean_io_result_mk_ok(lean::mk_option_some(lean_mk_string(msg)));
-    } else {
-      return lean_io_result_mk_ok(lean::mk_option_none());
-    }
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_count_basic_blocks(size_t ctx, size_t fn_val,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMValueRef fn_ref = lean_to_Value(fn_val);
-    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)LLVMCountBasicBlocks(fn_ref)));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_get_entry_basic_block(size_t ctx, size_t fn_val,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMValueRef fn_ref = lean_to_Value(fn_val);
-    LLVMBasicBlockRef bb_ref = LLVMGetEntryBasicBlock(fn_ref);
-    return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(bb_ref)));
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_get_first_instruction(size_t ctx, size_t bb,
-    lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMBasicBlockRef bb_ref = lean_to_BasicBlock(bb);
-    LLVMValueRef instr_ref = LLVMGetFirstInstruction(bb_ref);
-    if (instr_ref == NULL) {
-       return lean_io_result_mk_ok(lean::mk_option_none());
-    } else {
-       return lean_io_result_mk_ok(lean::mk_option_some(lean_box_usize(Value_to_lean(instr_ref))));
-    }
-#endif  // LEAN_LLVM
-}
-
-extern "C" LEAN_EXPORT lean_object *lean_llvm_position_builder_before(
-    size_t ctx, size_t builder, size_t instr, lean_object * /* w */) {
-#ifndef LEAN_LLVM
-    lean_always_assert(
-        false && ("Please build a version of Lean4 with -DLLVM=ON to invoke "
-                  "the LLVM backend function."));
-#else
-    LLVMPositionBuilderBefore(lean_to_Builder(builder), lean_to_Value(instr));
-    return lean_io_result_mk_ok(lean_box(0));
-#endif  // LEAN_LLVM
-}