awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDiffAt[s] f x
neg :
  Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))) 0
    (fderivWithin 𝕜 f s x)
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x) (fderivWithin 𝕜 f s x)

Tactic:
simp only [mfderivWithin, h, if_neg, not_false_iff]

Premises used: mfderivWithin, not_false_iff, if_neg
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDiffAt[s] f x
⊢ ¬DifferentiableWithinAt 𝕜 f s x

Tactic:
rw [mdifferentiableWithinAt_iff_differentiableWithinAt] at h

Premises used: mdifferentiableWithinAt_iff_differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))) 0
    (fderivWithin 𝕜 f s x)

Tactic:
(fderivWithin_zero_of_not_differentiableWithinAt h).symm

Premises used: instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, fderivWithin_zero_of_not_differentiableWithinAt, Eq.symm, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x))) 0
    (fderivWithin 𝕜 f s x)

Tactic:
exact (fderivWithin_zero_of_not_differentiableWithinAt h).symm

Premises used: fderivWithin_zero_of_not_differentiableWithinAt, Eq.symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
rw :
  Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x) (fderivWithin 𝕜 f Set.univ x)
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderiv% f x) (fderiv 𝕜 f x)

Tactic:
rw [← mfderivWithin_univ, ← fderivWithin_univ]

Premises used: fderivWithin_univ, mfderivWithin_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x) (fderivWithin 𝕜 f Set.univ x)

Tactic:
mfderivWithin_eq_fderivWithin

Premises used: mfderivWithin_eq_fderivWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (TangentSpace 𝓘(𝕜, E) x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x) (fderivWithin 𝕜 f Set.univ x)

Tactic:
exact mfderivWithin_eq_fderivWithin

Premises used: mfderivWithin_eq_fderivWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
s : Set M
t : Set F
x : M
hg : DifferentiableWithinAt 𝕜 g t (f x)
hf : MDiffAt[s] f x
h : MapsTo f s t
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
hg.mdifferentiableWithinAt.comp x hf h

Premises used: DifferentiableWithinAt.mdifferentiableWithinAt, MDifferentiableWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
s : Set M
x : M
hg : DifferentiableAt 𝕜 g (f x)
hf : MDiffAt[s] f x
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
hg.mdifferentiableAt.comp_mdifferentiableWithinAt x hf

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt, DifferentiableAt.mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
x : M
hg : DifferentiableAt 𝕜 g (f x)
hf : MDiffAt f x
⊢ MDiffAt (g ∘ f) x

Tactic:
hg.comp_mdifferentiableWithinAt hf

Premises used: MDifferentiableAt, DifferentiableAt.comp_mdifferentiableWithinAt, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
s : Set M
x : M
hg : Differentiable 𝕜 g
hf : MDiffAt[s] f x
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
hg.differentiableAt.comp_mdifferentiableWithinAt hf

Premises used: Differentiable.differentiableAt, DifferentiableAt.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
x : M
hg : Differentiable 𝕜 g
hf : MDiffAt f x
⊢ MDiffAt (g ∘ f) x

Tactic:
hg.comp_mdifferentiableWithinAt hf

Premises used: MDifferentiableAt, Differentiable.comp_mdifferentiableWithinAt, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
F' : Type u_11
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜 F'
g : F → F'
f : M → F
hg : Differentiable 𝕜 g
hf : MDiff f
⊢ MDiff (g ∘ f)

Tactic:
fun x ↦ hg.differentiableAt.comp_mdifferentiableAt (hf x)

Premises used: Differentiable.differentiableAt, MDifferentiable, DifferentiableAt.comp_mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
F : Type u_18
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
f : M → F
hf : MDiffAt[s] f x
⊢ DifferentiableWithinAt 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
simpa [extChartAt_self_eq] using (mdifferentiableWithinAt_iff.1 hf).2

Premises used: extChartAt_self_eq, And.right, mdifferentiableWithinAt_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
F : Type u_18
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
f : M → F
inst_8 : IsManifold I 1 M
hf :
  DifferentiableWithinAt 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt[s] f x

Tactic:
(mdifferentiableWithinAt_iff_source_of_mem_source (mem_chart_source H x)).2 ?_

Premises used: Iff.mpr, mem_chart_source, mdifferentiableWithinAt_iff_source_of_mem_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
F : Type u_18
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
f : M → F
inst_8 : IsManifold I 1 M
hf :
  DifferentiableWithinAt 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
refine :
  MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt[s] f x

Tactic:
refine (mdifferentiableWithinAt_iff_source_of_mem_source (mem_chart_source H x)).2 ?_

Premises used: Iff.mpr, mem_chart_source, mdifferentiableWithinAt_iff_source_of_mem_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
x : M
F : Type u_18
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
f : M → F
inst_8 : IsManifold I 1 M
hf :
  DifferentiableWithinAt 𝕜 (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
⊢ MDiffAt[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
simpa [extChartAt_self_eq] using hf.mdifferentiableWithinAt

Premises used: DifferentiableWithinAt.mdifferentiableWithinAt, extChartAt_self_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₁ →L[𝕜] F₂
s : Set M
x : M
hf : MDiffAt[s] f x
⊢ (MDiffAt[s] fun (y : M) ↦ ContinuousLinearMap.precomp F₃ (f y)) x

Tactic:
Differentiable.comp_mdifferentiableWithinAt
    (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip) hf

Premises used: Differentiable.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₁ →L[𝕜] F₂
x : M
hf : MDiffAt f x
⊢ (MDiffAt fun (y : M) ↦ ContinuousLinearMap.precomp F₃ (f y)) x

Tactic:
Differentiable.comp_mdifferentiableAt
    (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip) hf

Premises used: Differentiable.comp_mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₁ →L[𝕜] F₂
s : Set M
hf : MDiff[s] f
⊢ MDiff[s] fun (y : M) ↦ ContinuousLinearMap.precomp F₃ (f y)

Tactic:
fun x hx ↦ (hf x hx).clm_precomp

Premises used: MDifferentiableWithinAt.clm_precomp, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₁ →L[𝕜] F₂
hf : MDiff f
⊢ MDiff fun (y : M) ↦ ContinuousLinearMap.precomp F₃ (f y)

Tactic:
fun x ↦ (hf x).clm_precomp

Premises used: MDifferentiableAt.clm_precomp, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₂ →L[𝕜] F₃
s : Set M
x : M
hf : MDiffAt[s] f x
⊢ (MDiffAt[s] fun (y : M) ↦ ContinuousLinearMap.postcomp F₁ (f y)) x

Tactic:
Differentiable.comp_mdifferentiableWithinAt
    (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃)) hf

Premises used: Differentiable.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₂ →L[𝕜] F₃
x : M
hf : MDiffAt f x
⊢ (MDiffAt fun (y : M) ↦ ContinuousLinearMap.postcomp F₁ (f y)) x

Tactic:
Differentiable.comp_mdifferentiableAt
    (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃)) hf

Premises used: Differentiable.comp_mdifferentiableAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₂ →L[𝕜] F₃
s : Set M
hf : MDiff[s] f
⊢ MDiff[s] fun (y : M) ↦ ContinuousLinearMap.postcomp F₁ (f y)

Tactic:
fun x hx ↦
  (hf x hx).clm_postcomp

Premises used: MDifferentiableOn, MDifferentiableWithinAt.clm_postcomp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
f : M → F₂ →L[𝕜] F₃
hf : MDiff f
⊢ MDiff fun (y : M) ↦ ContinuousLinearMap.postcomp F₁ (f y)

Tactic:
fun x ↦ (hf x).clm_postcomp

Premises used: MDifferentiableAt.clm_postcomp, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ (MDiffAt[s] fun (x : M) ↦ g x ∘SL f x) x

Tactic:
Differentiable.comp_mdifferentiableWithinAt
    (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2)
    (f := fun x => (g x, f x)) (differentiable_fst.clm_comp differentiable_snd)
    (hg.prodMk_space hf)

Premises used: ContinuousLinearMap.comp, Differentiable.clm_comp, MDifferentiableWithinAt.prodMk_space, differentiable_snd, Differentiable.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₁
x : M
hg : MDiffAt g x
hf : MDiffAt f x
⊢ (MDiffAt fun (x : M) ↦ g x ∘SL f x) x

Tactic:
(hg.mdifferentiableWithinAt.clm_comp hf.mdifferentiableWithinAt).mdifferentiableAt Filter.univ_mem

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableWithinAt.clm_comp, MDifferentiableWithinAt.mdifferentiableAt, Filter.univ_mem
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
F₃ : Type u_16
inst_10 : NormedAddCommGroup F₃
inst_11 : NormedSpace 𝕜 F₃
g : M → F₁ →L[𝕜] F₃
f : M → F₂ →L[𝕜] F₁
s : Set M
hg : MDiff[s] g
hf : MDiff[s] f
⊢ MDiff[s] fun (x : M) ↦ g x ∘SL f x

Tactic:
fun x hx ↦ (hg x hx).clm_comp (hf x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.clm_comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
apply : Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2
⊢ DifferentiableWithinAt 𝕜 (F := F₂) (fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt

Premises used: Differentiable.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
differentiable_fst.clm_apply differentiable_snd

Premises used: differentiable_snd, Differentiable.clm_apply
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ Differentiable 𝕜 (F := F₂) fun (x : (F₁ →L[𝕜] F₂) × F₁) ↦ (x.1 : (a : F₁) → F₂) x.2

Tactic:
exact differentiable_fst.clm_apply differentiable_snd

Premises used: Differentiable.clm_apply
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F₁ : Type u_14
inst_6 : NormedAddCommGroup F₁
inst_7 : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst_8 : NormedAddCommGroup F₂
inst_9 : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ MapsTo (β := (F₁ →L[𝕜] F₂) × F₁) (fun (x : M) ↦ (g x, f x)) s univ

Tactic:
simp_rw [mapsTo_univ]

Premises used: Set.mapsTo_univ