From b5132a02137e483d6c2f3ed51cf845b6b083d2aa Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 3 Feb 2025 18:52:26 -0500 Subject: [PATCH] fix: harmonize with `List` --- Batteries/Data/Fin/Lemmas.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index e43a6dc7d2..d0265b03c2 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -33,9 +33,15 @@ theorem findSome?_succ {f : Fin (n+1) → Option α} : @[simp] theorem findSome?_succ_of_some {f : Fin (n+1) → Option α} (h : f 0 = some x) : findSome? f = some x := by simp [findSome?_succ, h] +@[simp] theorem findSome?_succ_of_isSome {f : Fin (n+1) → Option α} (h : (f 0).isSome) : + findSome? f = f 0 := by cases _h : f 0 <;> simp_all + @[simp] theorem findSome?_succ_of_none {f : Fin (n+1) → Option α} (h : f 0 = none) : findSome? f = findSome? fun i => f i.succ := by simp [findSome?_succ, h] +@[simp] theorem findSome?_succ_of_isNone {f : Fin (n+1) → Option α} (h : (f 0).isNone) : + findSome? f = findSome? fun i => f i.succ := by simp_all + theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f = some x) : ∃ i, f i = some x := by induction n with @@ -90,7 +96,6 @@ theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f match exists_of_findSome?_eq_some h with | ⟨i, h⟩ => rw [hf] at h; contradiction - theorem findSome?_isNone_iff {f : Fin n → Option α} : (findSome? f).isNone ↔ ∀ i, (f i).isNone := by simp