golf

EtienneC30 · EtienneC30 · commit 38ca5c28ccb4 · 2026-03-29T13:22:18.000+02:00
diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -733,11 +733,8 @@ theorem prod_take_ofFn {n : ℕ} (f : Fin n → M) (i : ℕ) :
     · have : i < length (ofFn f) := by rwa [length_ofFn]
       rw [prod_take_succ _ _ this]
       have A : ({j | j.val < i + 1} : Finset (Fin n)) =
-          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by
-        ext ⟨_, _⟩
-        simp [Nat.lt_succ_iff_lt_or_eq, or_comm]
-      rw [A, prod_insert (by simp), IH, mul_comm]
-      simp
+          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
+      grind
     · have A : (ofFn f).take i = (ofFn f).take i.succ := by
         rw [← length_ofFn (f := f)] at h
         have : length (ofFn f) ≤ i := not_lt.mp h
