chore: variants of dite_eq_left_iff (#8357)

This PR adds variants of `dite_eq_left_iff` that will be useful in a
future PR.

Author: TwoFX

src/Init/Data/Array/OfFn.lean

@@ -26,12 +26,11 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
   ext i h₁ h₂
   · simp
-  · simp [getElem_push]
-    split <;> rename_i h₃
-    · rfl
-    · congr
-      simp at h₁ h₂
-      omega
+  · simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
+      Nat.not_lt]
+    simp only [size_ofFn] at h₁
+    intro h₃
+    simp only [show i = n by omega]
 
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp

src/Init/Data/BitVec/Lemmas.lean

@@ -2261,7 +2261,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
+  simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
   by_cases h₂ : n + i < w
   · simp [h₂]
   · simp only [h₂, ↓reduceIte]

src/Init/PropLemmas.lean

@@ -692,24 +692,48 @@ attribute [local simp] Decidable.imp_iff_left_iff
 @[simp] theorem dite_eq_right_iff {p : Prop} [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by
   split <;> simp_all
 
+@[simp] theorem left_eq_dite_iff {p : Prop} [Decidable p] {x : α} {y : ¬ p → α} : x = (if h : p then x else y h) ↔ ∀ h : ¬ p, x = y h := by
+  split <;> simp_all
+
+@[simp] theorem right_eq_dite_iff {p : Prop} [Decidable p] {x : p → α} {y : α} : y = (if h : p then x h else y) ↔ ∀ h : p, y = x h := by
+  split <;> simp_all
+
 @[simp] theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by
   split <;> simp_all
 
 @[simp] theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by
   split <;> simp_all
 
+@[simp] theorem left_iff_dite_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p → Prop} : (x ↔ (if h : p then x else y h)) ↔ ∀ h : ¬ p, x ↔ y h := by
+  split <;> simp_all
+
+@[simp] theorem right_iff_dite_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : (y ↔ (if h : p then x h else y)) ↔ ∀ h : p, y ↔ x h := by
+  split <;> simp_all
+
 @[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ↔ ¬ p → y = x := by
   split <;> simp_all
 
 @[simp] theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y := by
   split <;> simp_all
 
+@[simp] theorem left_eq_ite_iff {p : Prop} [Decidable p] {x y : α} : x = (if p then x else y) ↔ ¬ p → x = y := by
+  split <;> simp_all
+
+@[simp] theorem right_eq_ite_iff {p : Prop} [Decidable p] {x y : α} : y = (if p then x else y) ↔ p → y = x := by
+  split <;> simp_all
+
 @[simp] theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by
   split <;> simp_all
 
 @[simp] theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y := by
   split <;> simp_all
 
+@[simp] theorem left_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} : (x ↔ (if p then x else y)) ↔ ¬ p → x = y := by
+  split <;> simp_all
+
+@[simp] theorem right_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} : (y ↔ (if p then x else y)) ↔ p → y = x := by
+  split <;> simp_all
+
 @[simp] theorem dite_then_false {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h := by
   split <;> simp_all
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -109,7 +109,7 @@ def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : I
         qs := qs.set i q₁
     else
       have : i < n := h.upper
-      have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta [Nat.max_def]; split <;> simp [*]
+      have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta only [Nat.max_def, right_eq_ite_iff]; split <;> simp [*]
       have : i < qs₂.size := by omega
       let q₂ ← qs₂[i].mulMonM k₂ m₂
       qs := qs.set i q₂

src/Std/Data/Internal/List/Associative.lean

@@ -5911,7 +5911,7 @@ theorem minEntry?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
     have := isSome_minEntry?_of_containsKey hc
     cases h : minEntry? l
     · simp_all
-    · simp
+    · simp only [Option.some.injEq]
       split
       · have := minKey?_le_of_containsKey hd hc (by simp [minKey?, h]; rfl)
         simp_all [← OrientedCmp.gt_iff_lt]