chore: bool and prop lemmas for Mathlib compatibility and improved confluence

doc/examples/bintree.lean

@@ -277,14 +277,13 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
     . by_cases' key < k
       cases h; apply ihr; assumption
 
-theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
+theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
         : (b.insert k v).find? k' = b.find? k' := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros
-    have_eq k k'
-    contradiction
+    intros le
+    exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
     specialize ihl bl

src/Init/ByCases.lean

@@ -37,15 +37,6 @@ 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]

src/Init/Classical.lean

@@ -125,16 +125,15 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
 /-- 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_not : ¬¬a ↔ a := Decidable.not_not
 
-@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
+@[simp low] 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 _
 
@@ -147,8 +146,22 @@ theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_an
 
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
+@[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
+@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
+
+@[simp] theorem and_or_imp : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
+
+@[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
+
+@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
+  Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
+            (fun a => And.intro (fun _ => a) (fun _ => a))
+
 end Classical
 
+/- Export for Mathlib compat. -/
+export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
+
 /-- 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

src/Init/Core.lean

@@ -677,7 +677,7 @@ You can prove theorems about the resulting element by induction on `h`, since
 theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
   h₁ ▸ h₂
 
-theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
+@[simp] theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
   rfl
 
 /--
@@ -1403,9 +1403,9 @@ theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro Fals
 
 theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro
 
-@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
+@[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id
 
-theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
+@[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
 
 theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip