awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderiv 𝕜 f x) : (a : E) → F)
simp :
  ∀ (hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f univ x) : (a : E) → F)),
    DifferentiableWithinAt 𝕜 f univ x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢

Premises used: fderivWithin_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f univ x) : (a : E) → F)
⊢ DifferentiableWithinAt 𝕜 f univ x

Tactic:
differentiableWithinAt_of_fderivWithin_injective hf

Premises used: differentiableWithinAt_of_fderivWithin_injective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(fderivWithin 𝕜 f univ x) : (a : E) → F)
⊢ DifferentiableWithinAt 𝕜 f univ x

Tactic:
exact differentiableWithinAt_of_fderivWithin_injective hf

Premises used: differentiableWithinAt_of_fderivWithin_injective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
s : Set E
hf : ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 f s x)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
differentiableWithinAt_of_fderivWithin_injective hf.injective

Premises used: differentiableWithinAt_of_fderivWithin_injective, ContinuousLinearMap.IsInvertible.injective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : ContinuousLinearMap.IsInvertible (fderiv 𝕜 f x)
⊢ DifferentiableAt 𝕜 f x

Tactic:
differentiableAt_of_fderiv_injective hf.injective

Premises used: differentiableAt_of_fderiv_injective, ContinuousLinearMap.IsInvertible.injective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
h : x ∉ tsupport f
⊢ f =ᶠ[𝓝 x] 0

Tactic:
rw [notMem_tsupport_iff_eventuallyEq] at h

Premises used: notMem_tsupport_iff_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x

Tactic:
(hasStrictFDerivAt_const (0 : F) x).congr_of_eventuallyEq h.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, hasStrictFDerivAt_const, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x

Tactic:
exact (hasStrictFDerivAt_const (0 : F) x).congr_of_eventuallyEq h.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, hasStrictFDerivAt_const, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
h : x ∉ tsupport f
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x

Tactic:
(HasStrictFDerivAt.of_notMem_tsupport 𝕜 h).hasFDerivAt

Premises used: HasStrictFDerivAt.of_notMem_tsupport, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
s : Set E
x : E
h : x ∉ tsupport f
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x

Tactic:
(HasFDerivAt.of_notMem_tsupport 𝕜 h).hasFDerivWithinAt

Premises used: HasFDerivAt.of_notMem_tsupport, HasFDerivAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
h : f =ᶠ[𝓝 x] 0
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0

Tactic:
simp [h.fderiv_eq]

Premises used: Filter.EventuallyEq.fderiv_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
rw : x ∉ tsupport f → Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0
⊢ x ∈ support (M := E →L[𝕜] F) (fderiv 𝕜 f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, notMem_support]

Premises used: Function.notMem_support, not_imp_not
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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 ∉ tsupport f → Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0

Tactic:
fderiv_of_notMem_tsupport _

Premises used: fderiv_of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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 ∉ tsupport f → Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0

Tactic:
exact fderiv_of_notMem_tsupport _

Premises used: fderiv_of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
⊢ tsupport (α := E →L[𝕜] F) (fderiv 𝕜 f) ⊆ tsupport f

Tactic:
closure_minimal (support_fderiv_subset 𝕜) isClosed_closure

Premises used: closure_minimal, tsupport, support_fderiv_subset, isClosed_closure
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
v : E
⊢ (tsupport.{u_2, u_3} (α := F) fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) v) ⊆ tsupport f

Tactic:
(tsupport_comp_subset (g := fun L : E →L[𝕜] F ↦ L v) rfl _).trans (tsupport_fderiv_subset 𝕜)

Premises used: HasSubset.Subset.trans, tsupport_fderiv_subset, tsupport_comp_subset, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : HasCompactSupport f
⊢ HasCompactSupport (β := E →L[𝕜] F) (fderiv 𝕜 f)

Tactic:
hf.mono' <| support_fderiv_subset 𝕜

Premises used: HasCompactSupport.mono', support_fderiv_subset
-- Module: Mathlib.Analysis.Calculus.FDeriv.Const
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
hf : HasCompactSupport f
v : E
⊢ HasCompactSupport.{u_2, u_3} (β := F) fun (x : E) ↦ (fderiv 𝕜 f x : (a : E) → F) v

Tactic:
hf.of_isClosed_subset (isClosed_tsupport _) (tsupport_fderiv_apply_subset 𝕜 v)

Premises used: isClosed_tsupport, IsCompact.of_isClosed_subset, tsupport_fderiv_apply_subset, HasCompactSupport
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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 ι
intro :
  ∀ (val : Fintype ι),
    HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
      HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
intro₁ :
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
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
⊢ HasStrictFDerivAt f f' x

Tactic:
rw [hasStrictFDerivAt_iff_isLittleOTVS] at h ⊢

Premises used: hasStrictFDerivAt_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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

Tactic:
Asymptotics.IsBigOTVS.trans_isLittleOTVS ?_ h

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
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)
⊢ 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:
refine Asymptotics.IsBigOTVS.trans_isLittleOTVS ?_ h

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
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))
⊢ 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:
simp only [Function.comp_apply, ← toContinuousMultilinearMapCLM_apply 𝕜,
      ContinuousLinearMap.comp_apply, ← map_sub]

Premises used: map_sub, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply, Function.comp_apply, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
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)
⊢ 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:
apply LinearMap.isBigOTVS_rev_comp

Premises used: LinearMap.isBigOTVS_rev_comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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
⊢ 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:
simp [isEmbedding_toContinuousMultilinearMap.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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 f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x

Tactic:
(toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x h

Premises used: ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
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 f f' x
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x

Tactic:
exact (toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x h

Premises used: ContinuousLinearMap.hasStrictFDerivAt, HasStrictFDerivAt.comp