From 5acbb59afdc0d19d424cf0bd93da6b7299097116 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 4 Oct 2024 10:08:32 +0200 Subject: [PATCH] fix --- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean index 797a612ad0b29..781bb36371121 100644 --- 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