awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableAt I I'' (g ∘ f) x

Tactic:
exact hg.comp _ hf

Premises used: MDifferentiableAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I' I'' g univ (f x)

Tactic:
rw [← mdifferentiableWithinAt_univ] at hg

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableWithinAt I I' f s x
hg₁ : MDifferentiableWithinAt I' I'' g univ (f x)
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
rw [← mdifferentiableWithinAt_univ] at hg

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hg : MDifferentiableWithinAt I' I'' g univ (f x)
hf : MDifferentiableWithinAt I I' f s x
⊢ s ⊆ f ⁻¹' univ

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hg : MDifferentiableWithinAt I' I'' g univ (f x)
hf : MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact hg.comp _ hf (by simp)

Premises used: MDifferentiableWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableWithinAt I I' f s x
hy : f x = y
⊢ MDifferentiableAt I' I'' g (f x)

Tactic:
subst hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hf : MDifferentiableWithinAt I I' f s x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
hg.comp_mdifferentiableWithinAt _ hf

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
hf : MDifferentiableWithinAt I I' f s x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact hg.comp_mdifferentiableWithinAt _ hf

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
apply :
  HasMFDerivWithinAt I I'' (g ∘ f) s x
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))

Tactic:
apply HasMFDerivWithinAt.mfderivWithin _ hxs

Premises used: HasMFDerivWithinAt.mfderivWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I'' (g ∘ f) s x
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))

Tactic:
HasMFDerivWithinAt.comp x hg.hasMFDerivWithinAt hf.hasMFDerivWithinAt h

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I'' (g ∘ f) s x
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))

Tactic:
exact HasMFDerivWithinAt.comp x hg.hasMFDerivWithinAt hf.hasMFDerivWithinAt h

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
y : M'
hg : MDifferentiableWithinAt I' I'' g u y
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
hy : f x = y
subst :
  ∀ (hg : MDifferentiableWithinAt I' I'' g u (f x)),
    Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
      (mfderivWithin I I'' (g ∘ f) s x)
      (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x))
        (mfderivWithin I I' f s x))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' y) (mfderivWithin I' I'' g u y) (mfderivWithin I I' f s x))

Tactic:
subst hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))

Tactic:
mfderivWithin_comp x hg hf h hxs

Premises used: mfderivWithin_comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
g : M' → M''
u : Set M'
x : M
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hxs : UniqueMDiffWithinAt I s x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))

Tactic:
exact mfderivWithin_comp x hg hf h hxs

Premises used: mfderivWithin_comp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
⊢ s ∩ f ⁻¹' u ∈ 𝓝[s] x

Tactic:
have A : s ∩ f ⁻¹' u ∈ 𝓝[s] x := Filter.inter_mem self_mem_nhdsWithin h
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
apply : MDifferentiableWithinAt I I'' (g ∘ f) (s ∩ f ⁻¹' u) x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x) (mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x)

Tactic:
apply MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin _ hxs A

Premises used: MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) (s ∩ f ⁻¹' u) x

Tactic:
hg.comp _ (hf.mono inter_subset_left) inter_subset_right

Premises used: Set.inter_subset_left, MDifferentiableWithinAt.mono, MDifferentiableWithinAt.comp, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) (s ∩ f ⁻¹' u) x

Tactic:
exact hg.comp _ (hf.mono inter_subset_left) inter_subset_right

Premises used: Set.inter_subset_left, MDifferentiableWithinAt.mono, MDifferentiableWithinAt.comp, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x) (mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x)

Tactic:
have B : mfderivWithin I I'' (g ∘ f) s x = mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x := by
    apply MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin _ hxs A
    exact hg.comp _ (hf.mono inter_subset_left) inter_subset_right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
B :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderivWithin I I'' (g ∘ f) s x) (mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) (mfderivWithin I I' f (s ∩ f ⁻¹' u) x)

Tactic:
have C : mfderivWithin I I' f s x = mfderivWithin I I' f (s ∩ f ⁻¹' u) x :=
    MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin (hf.mono inter_subset_left) hxs A