From ad4fd54e0b0bd4ba655c949d03988611fb182bdb Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 14 Nov 2023 16:21:47 +1100
Subject: [PATCH] feat: upstream lemmas about if-then-else (#360)

---
 Std/Data/List/Lemmas.lean  |  2 +-
 Std/Data/Range/Lemmas.lean |  5 +++--
 Std/Data/Rat/Lemmas.lean   |  2 +-
 Std/Logic.lean             | 17 +++++++++++++++++
 4 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index cbb38c49a4..63eb21e8b1 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -1707,7 +1707,7 @@ variable [DecidableEq α]
 @[simp] theorem diff_nil (l : List α) : l.diff [] = l := rfl
 
 @[simp] theorem diff_cons (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂ := by
-  simp [List.diff]; split <;> simp [*, erase_of_not_mem]
+  simp_all [List.diff, erase_of_not_mem]
 
 theorem diff_cons_right (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.diff l₂).erase a := by
   apply Eq.symm; induction l₂ generalizing l₁ <;> simp [erase_comm, *]
diff --git a/Std/Data/Range/Lemmas.lean b/Std/Data/Range/Lemmas.lean
index a7b2558d44..791820c0bb 100644
--- a/Std/Data/Range/Lemmas.lean
+++ b/Std/Data/Range/Lemmas.lean
@@ -71,7 +71,7 @@ theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range)
         conv => lhs; rw [← Nat.one_mul stop]
         exact Nat.mul_le_mul_right stop hstep
       intro fuel; induction fuel with intro l i hle H h1 h2 init
-      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]; split <;> simp
+      | zero => simp [forIn'.loop, Nat.le_zero.1 h1]
       | succ fuel ih =>
         cases l with
         | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)]
@@ -93,7 +93,8 @@ theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
     suffices ∀ fuel i hl b, forIn'.loop r.start r.stop r.step (fun x _ => f x) fuel i hl b =
         forIn.loop f fuel i r.stop r.step b from (this _ ..).symm
     intro fuel; induction fuel <;> intro i hl b <;>
-      unfold forIn.loop forIn'.loop <;> simp [*] <;> split <;> try simp
+      unfold forIn.loop forIn'.loop <;> simp [*]
+    split
     · simp [if_neg (Nat.not_le.2 ‹_›)]
     · simp [if_pos (Nat.not_lt.1 ‹_›)]
   · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ ..
diff --git a/Std/Data/Rat/Lemmas.lean b/Std/Data/Rat/Lemmas.lean
index 15c620f09b..ef7947c59d 100644
--- a/Std/Data/Rat/Lemmas.lean
+++ b/Std/Data/Rat/Lemmas.lean
@@ -99,7 +99,7 @@ theorem mkRat_self (a : Rat) : mkRat a.num a.den = a := by
 theorem mk_eq_mkRat (num den nz c) : ⟨num, den, nz, c⟩ = mkRat num den := by
   simp [mk_eq_normalize, normalize_eq_mkRat]
 
-@[simp] theorem zero_mkRat (n) : mkRat 0 n = 0 := by simp [mkRat_def]; apply ite_self
+@[simp] theorem zero_mkRat (n) : mkRat 0 n = 0 := by simp [mkRat_def]
 
 @[simp] theorem mkRat_zero (n) : mkRat n 0 = 0 := by simp [mkRat_def]
 
diff --git a/Std/Logic.lean b/Std/Logic.lean
index 68a7d4aa88..36855da23f 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -512,6 +512,9 @@ theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p
     (∀ 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 -/
@@ -761,6 +764,20 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 @[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
+
 /-! ## miscellaneous -/
 
 attribute [simp] inline