Apply suggestions from code review

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

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 =>
-    split <;> (try simp) <;> split <;> (try simp)
+    intros
     have_eq k k'
     contradiction
   | node left key value right ihl ihr =>

src/Init.lean

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

src/Init/ByCases.lean

@@ -0,0 +1,74 @@
+/-
+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,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
-import Init.Core
-import Init.NotationExtra
+import Init.PropLemmas
 
 universe u v
 
@@ -112,8 +111,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 (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
-  | Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
+  | Or.inl ha => Or.inl (eq_true ha)
+  | Or.inr hn => Or.inr (eq_false hn)
 
 -- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
@@ -123,15 +122,36 @@ 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
 
-/--
-`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
+/-- 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
 
-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)
+/-- 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

src/Init/Core.lean

@@ -17,7 +17,9 @@ universe u v w
 at the application site itself (by comparison to the `@[inline]` attribute,
 which applies to all applications of the function).
 -/
-def inline {α : Sort u} (a : α) : α := a
+@[simp] def inline {α : Sort u} (a : α) : α := a
+
+theorem id.def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -32,8 +34,32 @@ 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. -/
@@ -78,6 +104,8 @@ 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`
@@ -126,6 +154,10 @@ 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`
@@ -525,9 +557,7 @@ theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p :=
   fun hn : ¬ p => hn h
 
 -- proof irrelevance is built in
-theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
-
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
 
 /--
 If `h : α = β` is a proof of type equality, then `h.mp : α → β` is the induced
@@ -575,8 +605,9 @@ 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.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 false_of_ne : a ≠ a → False := Ne.irrefl
 
@@ -588,8 +619,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 true_ne_false : ¬True = False := ne_false_of_self trivial
+theorem false_ne_true : False ≠ True := fun h => h.symm ▸ trivial
 
 end Ne
 
@@ -668,22 +699,29 @@ 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
-    (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
-    (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
+  Iff.intro (h₂.mp ∘ h₁.mp) (h₁.mpr ∘ h₂.mpr)
 
-theorem Iff.symm (h : a ↔ b) : b ↔ a :=
-  Iff.intro (Iff.mpr h) (Iff.mp h)
+-- This is needed for `calc` to work with `iff`.
+instance : Trans Iff Iff Iff where
+  trans := Iff.trans
 
-theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
-  Iff.intro Iff.symm Iff.symm
+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.of_eq (h : a = b) : a ↔ b :=
-  h ▸ Iff.refl _
+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 And.comm : a ∧ b ↔ b ∧ a := by
-  constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
+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
 
 /-! # Exists -/
 
@@ -883,8 +921,13 @@ protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (
   apply heq_of_eq
   apply Subsingleton.elim
 
-instance (p : Prop) : Subsingleton p :=
-  ⟨fun a b => proofIrrel a b⟩
+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 (Decidable p) :=
   Subsingleton.intro fun
@@ -895,6 +938,9 @@ 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}
@@ -1174,12 +1220,117 @@ 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⟩
 
-/-! # Quotients -/
+/-! # 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
 
 /-- 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.Classical
+import Init.ByCases
 
 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]
+        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl, -and_imp]
         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; intros; assumption
+  | zero => simp
   | 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,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Coe
-import Init.Classical
-import Init.SimpLemmas
+import Init.ByCases
 import Init.Data.Nat.Basic
 import Init.Data.List.Basic
 import Init.Data.Prod
@@ -539,13 +538,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] at this
+  simp [toNormPoly, Poly.norm, Poly.denote_eq, -eq_iff_iff] 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] at this
+  simp [toNormPoly, Poly.norm,Poly.denote_le, -eq_iff_iff] 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) :=
@@ -590,7 +589,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 propext <;> apply Iff.intro <;> intro h
+     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> 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 _)
@@ -637,7 +636,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]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
   · 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]
@@ -650,7 +649,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]
+  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
   · intro h
@@ -658,12 +657,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 at this
+  simp [-eq_iff_iff] 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 at this
+  simp [-eq_iff_iff] 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
@@ -712,7 +711,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 at h
+  simp [-eq_iff_iff] 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/PropLemmas.lean

@@ -0,0 +1,443 @@
+/-
+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,6 +31,9 @@ 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₂)),
@@ -93,11 +96,16 @@ 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)
@@ -114,6 +122,58 @@ 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
@@ -166,11 +226,13 @@ 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⟩

tests/lean/1079.lean.expected.out

@@ -5,4 +5,32 @@
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True
+[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

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:32-9:55: error: failed to elaborate eliminator, expected type is not available
+276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available

tests/lean/run/1549.lean

@@ -1,16 +1,12 @@
 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,12 +4,6 @@ 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,9 +1,3 @@
-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,12 +34,6 @@ 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,11 +526,7 @@ theorem State.update_le_update (h : σ' ≼ σ) : σ'.update x v ≼ σ.update x
       simp [*] at he
       assumption
     next =>
-      by_cases hxy : x = y <;> simp [*]
-      next => intros; assumption
-      next =>
-        intro he' ih
-        exact ih he'
+      by_cases hxy : x = y <;> simp_all
 
 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,6 +1,3 @@
-@[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
 
@@ -13,5 +10,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; intro h; cases h; contradiction
+  cases o; simp only [isSome_none, false_iff]; intro h; cases h; contradiction
   simp [exists_prop]

tests/lean/run/recInfo1.lean

@@ -10,9 +10,6 @@ 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/simp4.lean

@@ -56,8 +56,6 @@ 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,7 +21,8 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  fail_if_success simp (config := { decide := false })
+  simp (config := { decide := false })
+  -- Goal is now `⊢ "hello" = "world" → 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 [Bind.bind, pure] at h; split at h
+    · simp only [bind, decide_eq_true_eq, 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,10 +46,12 @@ 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]
+Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite]
 [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, (if h : 1 ≤ x then x else 0) = if h : 1 ≤ x then x else 0 ==> True
+[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
 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