From 7a6fa85ed1ed529cc110d0f3c1a204cc64f47409 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 6 Sep 2024 09:45:14 +1000 Subject: [PATCH] chore: fix binders on ite_eq_left_iff (#5268) --- src/Init/PropLemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index d363a35df0..1b49ab341a 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -640,7 +640,7 @@ attribute [local simp] Decidable.imp_iff_left_iff @[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 ite_eq_left_iff {p : Prop} [Decidable p] (x y : α) : (if p then x else y) = x ↔ ¬ p → y = x := by +@[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