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 ι
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 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
have h : Function.update (β := E) fa.2 j 0 j =
  (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        (fun (x : Option ι) ↦ fa) (some j) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
    j
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: 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 j : ι
h :
  Function.update (β := E) fa.2 j 0 j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some j) ((g, 0) : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (some j)).2
      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
have h₁ : ∀ (hij : j ≠ i),
  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: rcases eq_or_ne j i with rfl | hij
-- 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 : (i : ι) → E i
⊢ Eq.{v + 1} (α := F) (∑ i : ι, (fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i (g i)))
    (∑ x : ι,
      (fa.1 : (a : (i : ι) → E i) → F) fun (i : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some x) (0, g) (some i)).2
          i)
have h : ∀ (i : ι),
  Eq.{v + 1} (α := F) ((fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i (g i)) : F)
    ((fa.1 : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some i) (0, g) (some i_1)).2
          i_1 :
      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 : (i : ι) → E i
i : ι
⊢ Eq.{v + 1} (α := F) ((fa.1 : (a : (i : ι) → E i) → F) (Function.update (β := E) fa.2 i (g i)) : F)
    ((fa.1 : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦
        (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
              (fun (x : Option ι) ↦ fa) (some i) (0, g) (some i_1)).2
          i_1 :
      F)
have h : ∀ (j : ι),
  Function.update (β := E) fa.2 i (g i) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) (0, g) (some j)).2
      j
Tactic: congr with j
-- 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 : (i : ι) → E i
i j : ι
⊢ Function.update (β := E) fa.2 i (g i) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) (0, g) (some j)).2
      j
have h : Function.update (β := E) fa.2 j (g j) j =
  (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        (fun (x : Option ι) ↦ fa) (some j) (0, g) (some j)).2
    j
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: 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 : (i : ι) → E i
i j : ι
h :
  Function.update (β := E) fa.2 j (g j) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some j) (0, g) (some j)).2
      j
⊢ Function.update (β := E) fa.2 i (g i) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) (0, g) (some j)).2
      j
have h₁ : ∀ (hij : j ≠ i),
  Function.update (β := E) fa.2 i (g i) j =
    (Function.update (β := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
          (fun (x : Option ι) ↦ fa) (some i) (0, g) (some j)).2
      j
Tactic: rcases eq_or_ne j i with rfl | hij
-- 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 ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ HasStrictFDerivAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x
have h : (apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
    ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i =
  HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
      (apply 𝕜 E F (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
      ((f x, fun (x_1 : ι) ↦ g x_1 x).1.linearDeriv (M₁ := E) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
        ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
    f'.prod (ContinuousLinearMap.pi (φ := E) g')
Tactic: convert!
    ContinuousMultilinearMap.hasStrictFDerivAt_uncurry (f x, (g · x)) |>.comp x
      (hf.prodMk (hasStrictFDerivAt_pi.2 hg))
-- 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 ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasStrictFDerivAt f f' x
hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x
⊢ (apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
        (apply 𝕜 E F (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
        ((f x, fun (x_1 : ι) ↦ g x_1 x).1.linearDeriv (M₁ := E) (f x, fun (x_1 : ι) ↦ g x_1 x).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
      f'.prod (ContinuousLinearMap.pi (φ := E) g')
have h : ∀ (x_1 : G),
  Eq.{v + 1} (α := F)
    (((apply 𝕜 E F fun (x_2 : ι) ↦ g x_2 x) ∘SL f' +
            ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_2 : ι) ↦ g x_2 x) i ∘SL g' i :
          (a : G) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i) →L[𝕜] F)
              (apply 𝕜 E F (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
              ((f x, fun (x_2 : ι) ↦ g x_2 x).1.linearDeriv (M₁ := E) (f x, fun (x_2 : ι) ↦ g x_2 x).2 ∘SL
                ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i)) ∘SL
            f'.prod (ContinuousLinearMap.pi (φ := E) g') :
          (a : G) → F)
        x_1 :
      F)
Tactic: ext
-- 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 ι
G : Type u_4
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) G (E i)
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    x
have simp : ∀ (hf : HasFDerivWithinAt f f' univ x) (hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) univ x),
  HasFDerivWithinAt (fun (x : G) ↦ (f x : (a : (i : ι) → E i) → F) fun (x_1 : ι) ↦ g x_1 x)
    ((apply 𝕜 E F fun (x_1 : ι) ↦ g x_1 x) ∘SL f' +
      ∑ i : ι, (f x).toContinuousLinearMap (M₁ := E) (fun (x_1 : ι) ↦ g x_1 x) i ∘SL g' i)
    univ x
Tactic: simp only [← hasFDerivWithinAt_univ] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
⊢ Eq (α := Fin (n + 1))
    (Fin.succ
      (((Equiv.symm
              (Function.Embedding.toEquivRange
                (Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                  ((Equiv.embeddingFinSucc n ι :
                      (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                    e))) :
            (↑(range (ι := Fin n)
                    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                          ((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e)) :
                      (a : Fin n) → ι)) :
                Type u_4) ≃
              Fin n) :
          (a :
              (↑(range
                    (⇑((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e).fst :
                      (a : Fin n) → ι)) :
                Type u_4)) →
            Fin n)
        (Subtype.mk (p := fun (x : ι) ↦
          Membership.mem (γ := Set ι)
            (range (ι := Fin n)
              (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                    ((Equiv.embeddingFinSucc n ι :
                        (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                      e)) :
                (a : Fin n) → ι))
            x)
          ((e : (a : Fin (n + 1)) → ι) j) h'k)))
    ((e.toEquivRange.symm : (a : (↑(range (⇑e : (a : Fin (n + 1)) → ι)) : Type u_4)) → Fin (n + 1))
      (Subtype.mk (p := fun (x : ι) ↦
        Membership.mem (γ := Set ι) (range (ι := Fin (n + 1)) (⇑e : (a : Fin (n + 1)) → ι)) x)
        ((e : (a : Fin (n + 1)) → ι) j) ⋯))
have hj : j ≠ 0
Tactic: have hj : j ≠ 0 := by
    rintro rfl
    simp at h'k