merge

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

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,10 +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

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/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/List/Basic.lean

@@ -876,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/Basic.lean

@@ -147,7 +147,7 @@ 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

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,7 +637,7 @@ 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]
@@ -649,7 +650,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa
 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
@@ -657,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
@@ -711,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/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,27 +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`.)
--/
-macro (name := runMeta) "run_meta " elems:doSeq : command =>
-  `(command| run_elab (show MetaM Unit from do $elems))

src/Init/PropLemmas.lean

@@ -1,443 +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.resolve_left  (h: a ∨ b) (na : ¬a) : b := h.elim (absurd · na) id
-theorem Or.resolve_right (h: a ∨ b) (nb : ¬b) : a := h.elim id (absurd · nb)
-
-theorem Or.neg_resolve_left  (h : ¬a ∨ b) (ha : a) : b := h.elim (absurd ha) id
-theorem Or.neg_resolve_right (h : a ∨ ¬b) (nb : b) : a := h.elim id (absurd nb)
-
-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

@@ -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,9 +910,6 @@ syntax (name := repeat1') "repeat1' " tacticSeq : tactic
 syntax "and_intros" : tactic
 macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 
-/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
-syntax (name := runTac) "run_tac " doSeq : tactic
-
 end Tactic
 
 namespace Attr

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,24 +699,6 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
-@[builtin_command_elab runCmd]
-def elabRunCmd : CommandElab
-  | `(run_cmd $elems:doSeq) => do
-    ← 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
-    ← liftTermElabM <| Term.withDeclName `_run_elab <|
-      unsafe Term.evalTerm (CommandElabM Unit)
-        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(Command.liftTermElabM <| discard do $elems))
-  | _ => 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,9 +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.Compiler.ImplementedByAttr
 
 namespace Lean.Elab.Term
 open Meta
@@ -428,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
@@ -438,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
@@ -451,20 +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
-
 end Lean.Elab.Term

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/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
@@ -483,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/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

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 192, column := 42 },
+some { range := { pos := { line := 191, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 198, column := 31 },
+             endPos := { line := 197, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 192, column := 46 },
+  selectionRange := { pos := { line := 191, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 192, column := 58 },
+                      endPos := { line := 191, column := 58 },
                       endCharUtf16 := 58 } }

tests/lean/1079.lean.expected.out

@@ -5,32 +5,4 @@
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.unify] @forall_exists_index:1000, failed to unify
-      ∀ (h : ∃ x, ?p x), ?q h
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq:1000, failed to unify
-      ∀ (a : ?α), a = ?a' → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq':1000, failed to unify
-      ∀ (a : ?α), ?a' = a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_or_imp:1000, failed to unify
-      ∀ (a : ?α), a = ?a' ∨ ?q a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?f a = b → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_apply_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), b = ?f a → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff₂:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?p a → ?f a = b → ?q b
-    with
-      False → False
-[Meta.Tactic.simp.rewrite] @imp_self:1000, False → False ==> True
+[Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True

tests/lean/276.lean

@@ -6,4 +6,4 @@ set_option pp.all true in
 
 -- but `def` doesn't work
 -- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec'
-def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α)
+def PEmpty.elim {α : Sort v} := PEmpty.rec (fun _ => α)

tests/lean/276.lean.expected.out

@@ -1,3 +1,3 @@
 276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
 fun {α : Sort v} => @?m α : {α : Sort v} → @?m α
-276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available
+276.lean:9:32-9:55: error: failed to elaborate eliminator, expected type is not available

tests/lean/binder_predicates.lean

@@ -1,8 +0,0 @@
-#check ∃ x > 10, x = 15
-#check ∃ x < 10, x = 5
-#check ∃ x ≥ 10, x = 15
-#check ∃ x ≤ 10, x = 5
-#check ∀ x > 10, x ≠ 5
-#check ∀ x < 10, x ≠ 15
-#check ∀ x ≥ 10, x ≠ 5
-#check ∀ x ≤ 10, x ≠ 15

tests/lean/binder_predicates.lean.expected.out

@@ -1,8 +0,0 @@
-∃ x, x > 10 ∧ x = 15 : Prop
-∃ x, x < 10 ∧ x = 5 : Prop
-∃ x, x ≥ 10 ∧ x = 15 : Prop
-∃ x, x ≤ 10 ∧ x = 5 : Prop
-∀ (x : Nat), x > 10 → x ≠ 5 : Prop
-∀ (x : Nat), x < 10 → x ≠ 15 : Prop
-∀ (x : Nat), x ≥ 10 → x ≠ 5 : Prop
-∀ (x : Nat), x ≤ 10 → x ≠ 15 : Prop

tests/lean/evalLeak.lean

@@ -1,23 +0,0 @@
-import Lean
-
-#eval match true with | true => false | false => true
-
-open Lean Elab Command Meta
-#eval show CommandElabM Unit from do
-  match ([] : List Nat) with
-  | []  =>
-    liftCoreM <| addDecl <| Declaration.defnDecl {
-      name        := `foo
-      type        := Lean.mkConst ``Bool
-      levelParams := []
-      value       := Lean.mkConst ``true
-      hints       := .opaque
-      safety      := .safe
-    }
-  | _ => return ()
-
-#check foo
--- The auxiliary declarations created to elaborate the commands above
--- should not leak into the environment
-#check _eval.match_1 -- Should fail
-#check _eval.match_2 -- Should fail

tests/lean/evalLeak.lean.expected.out

@@ -1,4 +0,0 @@
-false
-foo : Bool
-evalLeak.lean:22:7-22:20: error: unknown identifier '_eval.match_1'
-evalLeak.lean:23:7-23:20: error: unknown identifier '_eval.match_2'

tests/lean/interactive/keywordCompletion.lean.expected.out

@@ -2,7 +2,6 @@
  "position": {"line": 4, "character": 10}}
 {"items":
  [{"label": "bin", "kind": 21, "detail": "Type 1"},
-  {"label": "binder_predicate", "kind": 14, "detail": "keyword"},
   {"label": "binop%", "kind": 14, "detail": "keyword"},
   {"label": "binop_lazy%", "kind": 14, "detail": "keyword"},
   {"label": "binrel%", "kind": 14, "detail": "keyword"},

tests/lean/run/1549.lean

@@ -1,12 +1,16 @@
 theorem not_mem_nil (a : Nat) : ¬ a ∈ [] := fun x => nomatch x
 
+theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬ p) :
+  (∀ h' : p, q h') ↔ True := sorry
+
 example (R : Nat → Prop) : (∀ (a' : Nat), a' ∈ [] → R a') := by
   simp only [forall_prop_of_false (not_mem_nil _)]
   exact fun _ => True.intro
 
-def Not.elim' {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
-theorem iff_of_true' (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
-theorem iff_true_intro' (h : a) : a ↔ True := iff_of_true h ⟨⟩
+
+def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
+theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
+theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩
 
 example {P : Prop} : ∀ (x : Nat) (_ : x ∈ []), P :=
 by

tests/lean/run/1842.lean

@@ -4,6 +4,12 @@ inductive List.Pairwise : List α → Prop
   | nil : Pairwise []
   | cons : ∀ {a : α} {l : List α}, (∀ {a} (_ : a' ∈ l), R a a') → Pairwise l → Pairwise (a :: l)
 
+theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+  ⟨fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩, fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩⟩
+
+theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
+  rw [← and_assoc, ← and_assoc, @And.comm a b]
+
 theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by
   induction l₁ <;> simp [*, and_left_comm]

tests/lean/run/2552.lean

@@ -1,4 +1,4 @@
-@[inline] def decidable_of_iff'' {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
+@[inline] def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
   decidable_of_decidable_of_iff h
 
 theorem LE.le.lt_or_eq_dec {a b : Nat} (hab : a ≤ b) : a < b ∨ a = b :=

tests/lean/run/968.lean

@@ -1,3 +1,9 @@
+theorem and_comm (a b : Prop) : (a ∧ b) = (b ∧ a) := sorry
+
+theorem and_assoc (a b c : Prop) : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)):= sorry
+
+theorem and_left_comm (a b c : Prop) : (a ∧ (b ∧ c)) = (b ∧ (a ∧ c)) := sorry
+
 example (p q r : Prop) : (p ∧ q ∧ r)
                        = (r ∧ p ∧ q) :=
 by simp only [and_comm, and_left_comm, and_assoc]

tests/lean/run/ac_rfl.lean

@@ -34,6 +34,12 @@ theorem le_of_not_le {a b : Nat} (h : ¬ a ≤ b) : b ≤ a :=
   · exact Iff.intro .inr fun | .inl xy => Nat.le_trans ‹_› ‹_› | .inr xz => ‹_›
   · exact Iff.intro .inl fun | .inl xy => ‹_› | .inr xz => Nat.le_trans ‹_› (le_of_not_le ‹_›)
 
+theorem or_assoc : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := by
+  by_cases p <;> by_cases q <;> by_cases r <;> simp_all
+
+theorem or_comm : p ∨ q ↔ q ∨ p := by
+  by_cases p <;> by_cases q <;> simp_all
+
 theorem max_assoc (n m k : Nat) : max (max n m) k = max n (max m k) :=
   le_ext (by simp [or_assoc])
 

tests/lean/run/constProp.lean

@@ -526,7 +526,11 @@ theorem State.update_le_update (h : σ' ≼ σ) : σ'.update x v ≼ σ.update x
       simp [*] at he
       assumption
     next =>
-      by_cases hxy : x = y <;> simp_all
+      by_cases hxy : x = y <;> simp [*]
+      next => intros; assumption
+      next =>
+        intro he' ih
+        exact ih he'
 
 theorem Expr.eval_constProp_of_sub (e : Expr) (h : σ' ≼ σ) : (e.constProp σ').eval σ = e.eval σ := by
   induction e with simp [*]

tests/lean/run/eq_some_iff_get_eq_issue.lean

@@ -1,3 +1,6 @@
+@[simp]
+theorem exists_prop {p q : Prop} : (∃ h : p, q) ↔ p ∧ q :=
+Iff.intro (fun ⟨hp, hq⟩ => And.intro hp hq) (fun ⟨hp, hq⟩ => Exists.intro hp hq)
 
 namespace Option
 
@@ -10,5 +13,5 @@ def get {α : Type u} : ∀ {o : Option α}, isSome o → α
 
 theorem eq_some_iff_get_eq {o : Option α} {a : α} :
   o = some a ↔ ∃ h : o.isSome, Option.get h = a := by
-  cases o; simp only [isSome_none, false_iff]; intro h; cases h; contradiction
+  cases o; simp; intro h; cases h; contradiction
   simp [exists_prop]

tests/lean/run/macro.lean

@@ -1,5 +1,3 @@
-namespace Test
-
 abbrev Set (α : Type) := α → Prop
 axiom setOf {α : Type} : (α → Prop) → Set α
 axiom mem {α : Type} : α → Set α → Prop
@@ -45,5 +43,3 @@ macro_rules
 | `(#check2 $e) => `(#check $e #check $e)
 
 #check2 1
-
-end Test

tests/lean/run/recInfo1.lean

@@ -10,6 +10,9 @@ def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit
 let info ← mkRecursorInfo declName majorPos?
 print (toString info)
 
+theorem Iff.elim {a b c} (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
+  h₁ h₂.1 h₂.2
+
 set_option trace.Meta true
 set_option trace.Meta.isDefEq false
 

tests/lean/run/replace_tac.lean

@@ -1,46 +0,0 @@
-/-
-Copyright (c) 2022 Arthur Paulino. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Arthur Paulino
--/
-
-example (h : Int) : Nat := by
-  replace h : Nat := 0
-  exact h
-
-example (h : Nat) : Nat := by
-  have h : Int := 0
-  assumption -- original `h` is not absent but...
-
-example (h : Nat) : Nat := by
-  replace h : Int := 0
-  fail_if_success assumption -- original `h` is absent now
-  replace h : Nat := 0
-  exact h
-
--- tests with `this`
-
-example : Nat := by
-  have : Int := 0
-  replace : Nat := 0
-  assumption
-
-example : Nat := by
-  have : Nat := 0
-  have : Int := 0
-  assumption -- original `this` is not absent but...
-
-example : Nat := by
-  have : Nat := 0
-  replace : Int := 0
-  fail_if_success assumption -- original `this` is absent now
-  replace : Nat := 0
-  assumption
-
--- trying to replace the type of a variable when the goal depends on it
-
-example {a : Nat} : a = a := by
-  replace a : Int := 0
-  have : Nat := by assumption -- old `a` is not gone
-  have : Int := by exact a    -- new `a` is of type `Int`
-  simp

tests/lean/run/run_cmd.lean

@@ -1,13 +0,0 @@
-import Lean
-open Lean Elab Tactic
-
-run_cmd logInfo m!"hello world"
-
-run_cmd unsafe do logInfo "!"
-
-example : True := by
-  run_tac
-    evalApplyLikeTactic MVarId.apply (← `(True.intro))
-
-example : True := by_elab
-  Term.elabTerm (← `(True.intro)) none

tests/lean/run/simp4.lean

@@ -56,6 +56,8 @@ theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
 
 theorem ex10 (y x : Nat) : y = 0 → x + 0 = 0 → x = 0 := by
   simp
+  intro h₁ h₂
+  simp [h₂]
 
 theorem ex11 : ∀ x : Nat, 0 + x + 0 = x := by
   simp

tests/lean/run/simp6.lean

@@ -21,8 +21,7 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  simp (config := { decide := false })
-  -- Goal is now `⊢ "hello" = "world" → False`
+  fail_if_success simp (config := { decide := false })
   simp (config := { decide := true })
 
 theorem ex8 : (10 + 2000 = 20) = False :=

tests/lean/run/wfOverapplicationIssue.lean

@@ -4,7 +4,7 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
     unfold anyM.loop
     intro h
     split at h
-    · simp only [bind, decide_eq_true_eq, pure] at h; split at h
+    · simp [Bind.bind, pure] at h; split at h
       next he => subst a; apply sizeOf_get_lt
       next => have ih := aux (j+1) h; assumption
     · contradiction

tests/lean/simp_trace.lean.expected.out

@@ -46,12 +46,10 @@ Try this: simp only [h, Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
 [Meta.Tactic.simp.rewrite] @eq_self:1000, x + 2 = x + 2 ==> True
-Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite]
+Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
-[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] @eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True
+[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if h : 1 ≤ x then x else 0 ==> True
 Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True