chore(FDeriv/Pi): golf (leanprover-community#35663)

Also drop an unneeded assumption `[Finite ι]`.

Author: urkud

Mathlib/Analysis/Calculus/FDeriv/Pi.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn, Heather Macbeth
 -/
 module
 
-public import Mathlib.Analysis.Calculus.FDeriv.Add
+public import Mathlib.Analysis.Calculus.FDeriv.Prod
 public import Mathlib.Analysis.Calculus.FDeriv.Const
 
 /-!
@@ -14,24 +14,17 @@ public import Mathlib.Analysis.Calculus.FDeriv.Const
 
 public section
 
-variable {𝕜 ι : Type*} [DecidableEq ι] [Finite ι] [NontriviallyNormedField 𝕜]
+variable {𝕜 ι : Type*} [DecidableEq ι] [NontriviallyNormedField 𝕜]
 variable {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
 
 @[fun_prop]
 theorem hasFDerivAt_update (x : ∀ i, E i) {i : ι} (y : E i) :
     HasFDerivAt (Function.update x i) (.pi (Pi.single i (.id 𝕜 (E i)))) y := by
-  set l := (ContinuousLinearMap.pi (Pi.single i (.id 𝕜 (E i))))
-  have update_eq : Function.update x i = (fun _ ↦ x) + l ∘ (· - x i) := by
-    ext t j
-    dsimp [l, Pi.single, Function.update]
-    split_ifs with hji
-    · subst hji
-      simp
-    · simp
-  rw [update_eq]
-  have := Fintype.ofFinite ι
-  convert (hasFDerivAt_const _ _).add (l.hasFDerivAt.comp y (hasFDerivAt_sub_const (x i)))
-  rw [zero_add, ContinuousLinearMap.comp_id]
+  rw [hasFDerivAt_pi]
+  intro j
+  rcases eq_or_ne j i with rfl | hij
+  · simpa using hasFDerivAt_id _
+  · simpa [hij] using hasFDerivAt_const _ _
 
 @[fun_prop]
 theorem hasFDerivAt_single {i : ι} (y : E i) :
@@ -40,7 +33,6 @@ theorem hasFDerivAt_single {i : ι} (y : E i) :
 
 theorem fderiv_update (x : ∀ i, E i) {i : ι} (y : E i) :
     fderiv 𝕜 (Function.update x i) y = .pi (Pi.single i (.id 𝕜 (E i))) :=
-  have := Fintype.ofFinite ι
   (hasFDerivAt_update x y).fderiv
 
 theorem fderiv_single {i : ι} (y : E i) :