awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H
inst_7 : Fintype ι
hc : HasFDerivAt c c' x
u : (i : ι) → M i
⊢ HasFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u)
    ((c'.flipMultilinear (E := M) : (a : (i : ι) → M i) → E →L[𝕜] H) u) x

Tactic:
(ContinuousMultilinearMap.apply 𝕜 M H u).hasFDerivAt.comp x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, LinearMap.mkContinuous, ContinuousMultilinearMap.apply, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Fintype ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
⊢ Eq (α := E →L[𝕜] H) (fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x)
    ((flipMultilinear (E := M) (fderivWithin 𝕜 c s x) : (a : (i : ι) → M i) → E →L[𝕜] H) u)

Tactic:
(hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.continuousMultilinear_apply_const, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Fintype ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
⊢ Eq (α := E →L[𝕜] H) (fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x)
    ((flipMultilinear (E := M) (fderiv 𝕜 c x) : (a : (i : ι) → M i) → E →L[𝕜] H) u)

Tactic:
(hc.hasFDerivAt.continuousMultilinear_apply_const u).fderiv

Premises used: HasFDerivAt.continuousMultilinear_apply_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
⊢ DifferentiableWithinAt.{u_1, u_2, u_7} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x

Tactic:
have := Fintype.ofFinite ι
  (hc.hasFDerivWithinAt.continuousMultilinear_apply_const u).differentiableWithinAt

Premises used: Fintype.ofFinite, HasFDerivWithinAt.continuousMultilinear_apply_const, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
⊢ DifferentiableAt.{u_1, u_2, u_7} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x

Tactic:
have := Fintype.ofFinite ι
  (hc.hasFDerivAt.continuousMultilinear_apply_const u).differentiableAt

Premises used: Fintype.ofFinite, HasFDerivAt.continuousMultilinear_apply_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableOn 𝕜 c s
u : (i : ι) → M i
⊢ DifferentiableOn.{u_1, u_2, u_7} 𝕜 (F := H) (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s

Tactic:
fun x hx ↦ (hc x hx).continuousMultilinear_apply_const u

Premises used: DifferentiableOn, DifferentiableWithinAt.continuousMultilinear_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : Differentiable 𝕜 c
u : (i : ι) → M i
⊢ Differentiable.{u_1, u_2, u_7} 𝕜 (F := H) fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u

Tactic:
fun x ↦ (hc x).continuousMultilinear_apply_const u

Premises used: Differentiable, DifferentiableAt.continuousMultilinear_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
m : E
have :
  ∀ (this : Fintype ι),
    Eq.{u_7 + 1} (α := H) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x : (a : E) → H) m : H)
      ((((fderivWithin 𝕜 c s x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
            (a : (i : ι) → M i) → H)
          u :
        H)
⊢ Eq.{u_7 + 1} (α := H) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x : (a : E) → H) m : H)
    ((((fderivWithin 𝕜 c s x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : (i : ι) → M i
m : E
this : Fintype ι
⊢ Eq.{u_7 + 1} (α := H) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) s x : (a : E) → H) m : H)
    ((((fderivWithin 𝕜 c s x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)

Tactic:
simp [fderivWithin_continuousMultilinear_apply_const hxs hc]

Premises used: fderivWithin_continuousMultilinear_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
have :
  ∀ (this : Fintype ι),
    Eq.{u_7 + 1} (α := H) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x : (a : E) → H) m : H)
      ((((fderiv 𝕜 c x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
            (a : (i : ι) → M i) → H)
          u :
        H)
⊢ Eq.{u_7 + 1} (α := H) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x : (a : E) → H) m : H)
    ((((fderiv 𝕜 c x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (M i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (M i)
H : Type u_7
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
this : Fintype ι
⊢ Eq.{u_7 + 1} (α := H) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : (i : ι) → M i) → H) u) x : (a : E) → H) m : H)
    ((((fderiv 𝕜 c x : (a : E) → ContinuousMultilinearMap 𝕜 M H) m : ContinuousMultilinearMap 𝕜 M H) :
          (a : (i : ι) → M i) → H)
        u :
      H)

Tactic:
simp [fderiv_continuousMultilinear_apply_const hc]

Premises used: fderiv_continuousMultilinear_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
inst_7 : Fintype ι
hc : HasStrictFDerivAt c c' x
u : ι → F
⊢ HasStrictFDerivAt.{u_1, u_2, u_4} (𝕜 := 𝕜) (F := G) (fun (x : E) ↦ (c x : (a : ι → F) → G) u)
    ((c'.flipAlternating : (a : ι → F) → E →L[𝕜] G) u) x

Tactic:
(ContinuousAlternatingMap.apply 𝕜 F G u).hasStrictFDerivAt.comp x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasStrictFDerivAt, ContinuousAlternatingMap.apply, HasStrictFDerivAt.comp, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
inst_7 : Fintype ι
hc : HasFDerivWithinAt c c' s x
u : ι → F
⊢ HasFDerivWithinAt.{u_1, u_2, u_4} (𝕜 := 𝕜) (F := G) (fun (x : E) ↦ (c x : (a : ι → F) → G) u)
    ((c'.flipAlternating : (a : ι → F) → E →L[𝕜] G) u) s x

Tactic:
(ContinuousAlternatingMap.apply 𝕜 F G u).hasFDerivAt.comp_hasFDerivWithinAt x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, ContinuousAlternatingMap.apply, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G
inst_7 : Fintype ι
hc : HasFDerivAt c c' x
u : ι → F
⊢ HasFDerivAt.{u_1, u_2, u_4} (𝕜 := 𝕜) (F := G) (fun (y : E) ↦ (c y : (a : ι → F) → G) u)
    ((c'.flipAlternating : (a : ι → F) → E →L[𝕜] G) u) x

Tactic:
(ContinuousAlternatingMap.apply 𝕜 F G u).hasFDerivAt.comp x hc

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, ContinuousAlternatingMap.apply, LinearMap.mkContinuous, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Fintype ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x)
    ((flipAlternating (fderivWithin 𝕜 c s x) : (a : ι → F) → E →L[𝕜] G) u)

Tactic:
(hc.hasFDerivWithinAt.continuousAlternatingMap_apply_const u).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.continuousAlternatingMap_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Fintype ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x)
    ((flipAlternating (fderiv 𝕜 c x) : (a : ι → F) → E →L[𝕜] G) u)

Tactic:
(hc.hasFDerivAt.continuousAlternatingMap_apply_const u).fderiv

Premises used: HasFDerivAt.continuousAlternatingMap_apply_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
⊢ DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x

Tactic:
have := Fintype.ofFinite ι
  (hc.hasFDerivWithinAt.continuousAlternatingMap_apply_const u).differentiableWithinAt

Premises used: Fintype.ofFinite, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.continuousAlternatingMap_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
⊢ DifferentiableAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x

Tactic:
have := Fintype.ofFinite ι
  (hc.hasFDerivAt.continuousAlternatingMap_apply_const u).differentiableAt

Premises used: Fintype.ofFinite, HasFDerivAt.continuousAlternatingMap_apply_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
have :
  ∀ (this : Fintype ι),
    Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x : (a : E) → G) m : G)
      ((((fderivWithin 𝕜 c s x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x : (a : E) → G) m : G)
    ((((fderivWithin 𝕜 c s x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
u : ι → F
m : E
this : Fintype ι
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s x : (a : E) → G) m : G)
    ((((fderivWithin 𝕜 c s x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)

Tactic:
simp [fderivWithin_continuousAlternatingMap_apply_const hxs hc]

Premises used: fderivWithin_continuousAlternatingMap_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
m : E
have :
  ∀ (this : Fintype ι),
    Eq.{u_4 + 1} (α := G) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x : (a : E) → G) m : G)
      ((((fderiv 𝕜 c x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)
⊢ Eq.{u_4 + 1} (α := G) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x : (a : E) → G) m : G)
    ((((fderiv 𝕜 c x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableAt 𝕜 c x
u : ι → F
m : E
this : Fintype ι
⊢ Eq.{u_4 + 1} (α := G) ((fderiv 𝕜 (fun (y : E) ↦ (c y : (a : ι → F) → G) u) x : (a : E) → G) m : G)
    ((((fderiv 𝕜 c x : (a : E) → F [⋀^ι]→L[𝕜] G) m : F [⋀^ι]→L[𝕜] G) : (a : ι → F) → G) u : G)

Tactic:
simp [fderiv_continuousAlternatingMap_apply_const hc]

Premises used: fderiv_continuousAlternatingMap_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : DifferentiableOn 𝕜 c s
u : ι → F
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (F := G) (fun (y : E) ↦ (c y : (a : ι → F) → G) u) s

Tactic:
fun x hx ↦ (hc x hx).continuousAlternatingMap_apply_const u

Premises used: DifferentiableWithinAt.continuousAlternatingMap_apply_const, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.CompCLM
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
ι : Type u_5
c : E → F [⋀^ι]→L[𝕜] G
inst_7 : Finite ι
hc : Differentiable 𝕜 c
u : ι → F
⊢ Differentiable.{u_1, u_2, u_4} 𝕜 (F := G) fun (y : E) ↦ (c y : (a : ι → F) → G) u

Tactic:
fun x ↦ (hc x).continuousAlternatingMap_apply_const u

Premises used: Differentiable, DifferentiableAt.continuousAlternatingMap_apply_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
this : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' (t \ {x}) x

Tactic:
simp only [HasFDerivWithinAt, this]

Premises used: HasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
suffices : 𝓝[s \ {x}] x = 𝓝[t \ {x}] x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' (t \ {x}) x

Tactic:
suffices 𝓝[s \ {x}] x = 𝓝[t \ {x}] x by simp only [HasFDerivWithinAt, this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ 𝓝[s \ {x}] x = 𝓝[t \ {x}] x

Tactic:
simpa only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter', diff_eq, inter_comm]
        using h

Premises used: Set.diff_eq, Set.inter_comm, Filter.set_eventuallyEq_iff_inf_principal, nhdsWithin_inter'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
h : s =ᶠ[𝓝 x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set_nhdsNE <| h.filter_mono inf_le_left

Premises used: Filter.EventuallyEq.filter_mono, hasFDerivWithinAt_congr_set_nhdsNE, inf_le_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
inl : ∀ (h : s =ᶠ[𝓝[≠] x] t), HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
inr : ∀ (hne : x ≠ y), HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
rcases eq_or_ne x y with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
h : s =ᶠ[𝓝[≠] x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set_nhdsNE h

Premises used: hasFDerivWithinAt_congr_set_nhdsNE
-- Module: Mathlib.Analysis.Calculus.FDeriv.Congr
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
f' : E →L[𝕜] F
x : E
s t : Set E
inst_7 : T1Space E
h : s =ᶠ[𝓝[≠] x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
exact hasFDerivWithinAt_congr_set_nhdsNE h

Premises used: hasFDerivWithinAt_congr_set_nhdsNE