awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
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))
⊢ 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

Tactic:
convert! Hf using 1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
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)
⊢ 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)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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 : ι
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
⊢ 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 j
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
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
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
j : ι
⊢ 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:
simp [*]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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 : ι
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:
simp [*]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
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)
⊢ 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)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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 : ι
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
⊢ 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 j
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
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
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
⊢ 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

Premises used: eq_or_ne, rfl