fix

leanprover-community · Oct 4, 2024 · 5acbb59 · 5acbb59
1 parent f84210d
commit 5acbb59
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
@@ -663,7 +663,7 @@ def extendEquiv (n : ℕ) :
         · intro j
           induction i using Fin.induction with
           | zero =>
-            simp only [cases_zero, cast_zero, coe_fin_one]
+            simp only [cases_zero, cast_zero, val_eq_zero]
             exact (apply_eq_of_range_eq_singleton h _).symm
           | succ i => simp
     · dsimp only