awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Const (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
⊢ x ∈ support (M := E →L[𝕜] F) (fderiv 𝕜 f) → x ∈ tsupport f
have rw : x ∉ tsupport f → Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0
Tactic: rw [← not_imp_not, notMem_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
have intro : ∀ (val : Fintype ι),
  HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
have intro : HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x → HasStrictFDerivAt f f' x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
intro :
  HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x →
    HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
have intro₁ : HasStrictFDerivAt f f' x → HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
h : HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x
⊢ HasStrictFDerivAt f f' x
have intro : ∀
  (h :
    Asymptotics.IsLittleOTVS 𝕜 (E := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (F := E)
      (𝓝 (x, x))
      (fun (p : E × E) ↦
        HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
          ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
          ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
              (p.1 - p.2) :
            ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H))
      fun (p : E × E) ↦ p.1 - p.2),
  Asymptotics.IsLittleOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F := E) (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
    fun (p : E × E) ↦ p.1 - p.2
Tactic: rw [hasStrictFDerivAt_iff_isLittleOTVS] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
h :
  Asymptotics.IsLittleOTVS 𝕜 (E := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (F := E)
    (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
        ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
        ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
            (p.1 - p.2) :
          ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H))
    fun (p : E × E) ↦ p.1 - p.2
⊢ Asymptotics.IsLittleOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F := E) (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
    fun (p : E × E) ↦ p.1 - p.2
have intro : Asymptotics.IsBigOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
  (𝓝 (x, x))
  (fun (p : E × E) ↦
    HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
  fun (p : E × E) ↦
  HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
    ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
    ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H) (p.1 - p.2) :
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
Tactic: refine Asymptotics.IsBigOTVS.trans_isLittleOTVS ?_ h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
h :
  Asymptotics.IsLittleOTVS 𝕜 (E := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (F := E)
    (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
        ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
        ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
            (p.1 - p.2) :
          ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H))
    fun (p : E × E) ↦ p.1 - p.2
⊢ Asymptotics.IsBigOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F :=
    ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
    fun (p : E × E) ↦
    HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
      ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
      ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H) (p.1 - p.2) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
have intro : Asymptotics.IsBigOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
  (𝓝 (x, x))
  (fun (p : E × E) ↦
    HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
  fun (p : E × E) ↦
  (toContinuousMultilinearMapCLM 𝕜 : (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
    (HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
Tactic: simp only [Function.comp_apply, ← toContinuousMultilinearMapCLM_apply 𝕜,
      ContinuousLinearMap.comp_apply, ← map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst_7 : Finite ι
val : Fintype ι
h :
  Asymptotics.IsLittleOTVS 𝕜 (E := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (F := E)
    (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
        ((toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2)
        ((toContinuousMultilinearMapCLM 𝕜 ∘SL f' : (a : E) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
            (p.1 - p.2) :
          ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H))
    fun (p : E × E) ↦ p.1 - p.2
⊢ Asymptotics.IsBigOTVS 𝕜 (E := G [⋀^ι]→L[𝕜] H) (F :=
    ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) (𝓝 (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
    fun (p : E × E) ↦
    (toContinuousMultilinearMapCLM 𝕜 : (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
      (HSub.hSub (β := G [⋀^ι]→L[𝕜] H) (f p.1 - f p.2) ((f' : (a : E) → G [⋀^ι]→L[𝕜] H) (p.1 - p.2) : G [⋀^ι]→L[𝕜] H))
have intro : LE.le (α := Filter (G [⋀^ι]→L[𝕜] H))
  (Filter.comap (β := ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
    (⇑((↑(toContinuousMultilinearMapCLM 𝕜) :
            G [⋀^ι]→L[𝕜] H →ₗ[𝕜] ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) :
          G [⋀^ι]→L[𝕜] H →ₗ[𝕜] ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H) :
      (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
    (𝓝 0))
  (𝓝 0)
Tactic: apply LinearMap.isBigOTVS_rev_comp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt (fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
    (HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
      G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
    fg
have rw : HasStrictFDerivAt
  (toContinuousMultilinearMap ∘ fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
  (toContinuousMultilinearMapCLM 𝕜 ∘SL
    HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
      G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
      (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
  fg
Tactic: rw [← hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt
    (toContinuousMultilinearMap ∘ fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
    fg
have H₁ : HasStrictFDerivAt
  (fun (fg : ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G)) ↦
    fg.1.compContinuousLinearMap (M₁ := fun (x : ι) ↦ F) (M₁' := fun (x : ι) ↦ G) fg.2)
  (HAdd.hAdd (α :=
    ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
      ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
    (β :=
    ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
      ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
    (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : ι) ↦ F) (E₁ := fun (x : ι) ↦ G)
          (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
          ((i : ι) → F →L[𝕜] G) :
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
    ((fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).1.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ F) (E₁ :=
          fun (x : ι) ↦ G) (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
        ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
          ((i : ι) → F →L[𝕜] G) :
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H))
  (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2)
Tactic: have H₁ := ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap
    (fg.1.1, fun _ : ι ↦ fg.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
H₁ :
  HasStrictFDerivAt
    (fun (fg : ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G)) ↦
      fg.1.compContinuousLinearMap (M₁ := fun (x : ι) ↦ F) (M₁' := fun (x : ι) ↦ G) fg.2)
    (HAdd.hAdd (α :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (β :=
      ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
        ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      (ContinuousMultilinearMap.compContinuousLinearMapL (E := fun (x : ι) ↦ F) (E₁ := fun (x : ι) ↦ G)
            (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H)
      ((fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).1.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ F)
            (E₁ := fun (x : ι) ↦ G) (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2).2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H)
            ((i : ι) → F →L[𝕜] G) :
        ContinuousMultilinearMap.{u_1, u_2, u_5, u_6} 𝕜 (fun (x : ι) ↦ G) H × ((i : ι) → F →L[𝕜] G) →L[𝕜]
          ContinuousMultilinearMap.{u_1, u_2, u_4, u_6} 𝕜 (fun (x : ι) ↦ F) H))
    (fg.1.toContinuousMultilinearMap, fun (x : ι) ↦ fg.2)
⊢ HasStrictFDerivAt
    (toContinuousMultilinearMap ∘ fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      HAdd.hAdd (α := G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H) (β :=
        G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H)
        (fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) :
          G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G) →L[𝕜] F [⋀^ι]→L[𝕜] H))
    fg
have H₂ : HasStrictFDerivAt
  (⇑(toContinuousMultilinearMapCLM 𝕜) : (a : G [⋀^ι]→L[𝕜] H) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) H)
  (toContinuousMultilinearMapCLM 𝕜) fg.1
Tactic: have H₂ := ((toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt (x := fg.1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x
have intro : ∀ (val : Fintype ι),
  DifferentiableWithinAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) s x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x
have intro : ∀ (val : Fintype ι), DifferentiableAt 𝕜 (F := F [⋀^ι]→L[𝕜] H) (fun (x : E) ↦ (f x).compContinuousLinearMap (g x)) x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst_7 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
⊢ DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x
have intro : ∀ (val : Fintype ι),
  DifferentiableWithinAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) s x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst_7 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x
have intro : ∀ (val : Fintype ι),
  DifferentiableAt.{u_1, u_3, u_5} 𝕜 (F := G) (fun (x : E) ↦ (f x : (a : ι → F) → G) fun (x_1 : ι) ↦ g x_1 x) x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
⊢ Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)
have intro : ∀ (val : Fintype ι), Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
val : Fintype ι
⊢ Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)
have intro : Differentiable 𝕜 (F := E [⋀^ι]→L[𝕜] F) fun (x : ι → E) ↦ f
Tactic: apply Differentiable.continuousAlternatingMap_apply
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Finite ι
f : E [⋀^ι]→L[𝕜] F
val : Fintype ι
intro : Differentiable 𝕜 (F := E [⋀^ι]→L[𝕜] F) fun (x : ι → E) ↦ f
⊢ Differentiable 𝕜 (E := ι → E) (F := F) (⇑f : (a : ι → E) → F)
have intro₁ : ∀ (i : ι), Differentiable 𝕜 (F := E) fun (x : ι → E) ↦ x i
Tactic: apply Differentiable.continuousAlternatingMap_apply