awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
rw : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - #s = 1
⊢ #sᶜ = 1
have rw₁ : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - (Fintype.card ι - 1) = 1
Tactic: rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
rw : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - #s = 1
rw₁ : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - (Fintype.card ι - 1) = 1
⊢ #sᶜ = 1
have rw₂ : 1 + (Fintype.card ι - 1) - (Fintype.card ι - 1) = 1
Tactic: rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
rw : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - #s = 1
rw₁ : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - (Fintype.card ι - 1) = 1
rw₂ : 1 + (Fintype.card ι - 1) - (Fintype.card ι - 1) = 1
⊢ #sᶜ = 1
have rw₃ : Eq (α := ℕ) 1 1
Tactic: rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)
have h : #sᶜ = 1
Tactic: have h : #sᶜ = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
⊢ ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)
have right : ∀ (a : Fin (1 + (Fintype.card ι - 1))) (ha : sᶜ = {a}),
  ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ sorry :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)
Tactic: obtain ⟨a, ha⟩ := card_eq_one.mp h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
i : ι
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Finset.piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
          (↑(((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
                    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ
                      ⋯) ∘
                  (⇑(Fintype.equivFinOfCardEq ⋯) : (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))))
                i) :
            Finset (Fin (1 + (Fintype.card ι - 1))))
          (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y) :
      F)
have h : Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
  ((domDomCongr (Fintype.equivFinOfCardEq sorry)
          (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E)
            (ContinuousLinearMap.proj (φ := E))) :
        (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
      (Function.update (β := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
          (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x)
          (((Fintype.equivFinOfCardEq sorry : ι ≃ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) :
              (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)))
            i)
          y :
        (a : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) :
    F)
Tactic: rw [Function.comp_apply, Subtype.coe_mk, compl_singleton, piecewise_erase_univ,
    toFormalMultilinearSeries, dif_pos (Nat.add_sub_of_le Fintype.card_pos).symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
i : ι
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((domDomCongr (Fintype.equivFinOfCardEq ⋯)
            (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E)
              (ContinuousLinearMap.proj (φ := E))) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Function.update (β := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
            (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x)
            (((Fintype.equivFinOfCardEq ⋯ : ι ≃ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) :
                (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)))
              i)
            y :
          (a : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) :
      F)
have h : Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
  ((f : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1 : F)
Tactic: simp_rw [domDomCongr_apply, compContinuousLinearMap_apply, ContinuousLinearMap.proj_apply,
    Function.update_apply, (Equiv.injective _).eq_iff, ite_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
i : ι
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1 : F)
have h : Function.update (β := E) x i (y i) = fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F) (f.linearDeriv (M₁ := E) x) x
have rw : HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F)
  ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
    (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1))
  x
Tactic: rw [← changeOrigin_toFormalMultilinearSeries]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1))
    x
have h : x = 0 + x
Tactic: convert! f.hasFiniteFPowerSeriesOnBall.hasStrictFDerivAt (y := x) ENNReal.coe_lt_top
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ x = 0 + x
have h : x = x
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F)
    (fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦ (fx.1 : (a : (i : ι) → E i) → F) fx.2)
    (HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
      (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
      (fa.1.linearDeriv (M₁ := E) fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)))
    fa
have Hf : HasStrictFDerivAt
  (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
    (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
      ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
  ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
      fa) ∘SL
    ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
      fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
  fa
Tactic: have Hf := (f.hasStrictFDerivAt (fun _ ↦ fa)).comp (f := fun fx _ ↦ fx) fa
    (hasStrictFDerivAt_pi.2 fun _ ↦ hasStrictFDerivAt_id _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F)
    (fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦ (fx.1 : (a : (i : ι) → E i) → F) fx.2)
    (HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
      (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
      (fa.1.linearDeriv (M₁ := E) fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)))
    fa
have h : Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
      (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
      Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
      (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) →
    Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
        UniformSpace.toTopologicalSpace →
      HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
          (apply 𝕜 E F fa.2 ∘SL ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
          (fa.1.linearDeriv (M₁ := E) fa.2 ∘SL
            ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) =
        (f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
            fun (x : Option ι) ↦ fa) ∘SL
          ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
            fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
Tactic: convert! Hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup
e_5 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
e_6 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
    UniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
⊢ Eq.{v + 1} (α := F) (∑ i : ι, (fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i 0))
    (∑ i : ι,
      (fa.1 : (a : (i : ι) → E i) → F) fun (j : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some i) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
          j)
have h : ∀ (i : ι),
  Eq.{v + 1} (α := F) ((fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i 0) : F)
    ((fa.1 : (a : (i : ι) → E i) → F) fun (j : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some i) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
          j :
      F)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) Prod.instAddCommGroup
    NormedAddCommGroup.toAddCommGroup
e_5 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (Prod.instModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) (β :=
    Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    (NormedSpace.toModule : Module 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
e_6 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))) instTopologicalSpaceProd
    UniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
i : ι
⊢ Eq.{v + 1} (α := F) ((fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i 0) : F)
    ((fa.1 : (a : (i : ι) → E i) → F) fun (j : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some i) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
          j :
      F)
have h : ∀ (j : ι),
  Function.update (β := E) fa.2 i 0 j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
      j
Tactic: congr with j