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
s : Set M
g : M' → M''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g univ (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I'' (g ∘ f) s x (g' ∘SL f')

Tactic:
HasMFDerivWithinAt.comp x (hg.mono (subset_univ _)) hf subset_preimage_univ

Premises used: Set.subset_univ, Set.subset_preimage_univ, HasMFDerivWithinAt.mono, 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''
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
g' : ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x)) (TangentSpace I'' (g (f x)))
hg : HasMFDerivWithinAt I' I'' g univ (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I'' (g ∘ f) s x (g' ∘SL f')

Tactic:
exact HasMFDerivWithinAt.comp x (hg.mono (subset_univ _)) hf subset_preimage_univ

Premises used: Set.subset_univ, Set.subset_preimage_univ, HasMFDerivWithinAt.mono, 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
rcases :
  ∀ (f' : E →L[𝕜] E')
    (hf' :
      HasFDerivWithinAt
        ((↑I' : H' → E') ∘
          ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
            (↑I.symm : E → H))
        f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑I : H → E) ((↑(chartAt H x) : M → H) x))),
    MDifferentiableWithinAt I I'' (g ∘ f) s x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
rcases hf.2 with ⟨f', hf'⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop
-- 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
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ HasMFDerivWithinAt I I' f s x f'

Tactic:
have F : HasMFDerivWithinAt I I' f s x f' := ⟨hf.1, hf'⟩
-- 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
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
F : HasMFDerivWithinAt I I' f s x f'
rcases :
  ∀ (g' : E' →L[𝕜] E'')
    (hg' :
      HasFDerivWithinAt
        ((↑I'' : H'' → E'') ∘
          ((↑(chartAt H'' (g (f x))) : M'' → H'') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M')) ∘
            (↑I'.symm : E' → H'))
        g'
        ((↑I'.symm : E' → H') ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M') ⁻¹' u ∩
          range (↑I' : H' → E'))
        ((↑I' : H' → E') ((↑(chartAt H' (f x)) : M' → H') (f x)))),
    MDifferentiableWithinAt I I'' (g ∘ f) s x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
rcases hg.2 with ⟨g', hg'⟩

Premises used: ChartedSpace.LiftPropWithinAt.prop
-- 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
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
F : HasMFDerivWithinAt I I' f s x f'
g' : E' →L[𝕜] E''
hg' :
  HasFDerivWithinAt
    ((↑I'' : H'' → E'') ∘
      ((↑(chartAt H'' (g (f x))) : M'' → H'') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M')) ∘
        (↑I'.symm : E' → H'))
    g'
    ((↑I'.symm : E' → H') ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M') ⁻¹' u ∩
      range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (f x)) : M' → H') (f x)))
⊢ HasMFDerivWithinAt I' I'' g u (f x) g'

Tactic:
have G : HasMFDerivWithinAt I' I'' g u (f x) g' := ⟨hg.1, hg'⟩
-- 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
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
F : HasMFDerivWithinAt I I' f s x f'
g' : E' →L[𝕜] E''
hg' :
  HasFDerivWithinAt
    ((↑I'' : H'' → E'') ∘
      ((↑(chartAt H'' (g (f x))) : M'' → H'') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M')) ∘
        (↑I'.symm : E' → H'))
    g'
    ((↑I'.symm : E' → H') ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M') ⁻¹' u ∩
      range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (f x)) : M' → H') (f x)))
G : HasMFDerivWithinAt I' I'' g u (f x) g'
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
(HasMFDerivWithinAt.comp x G F h).mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt, 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
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    f' ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
F : HasMFDerivWithinAt I I' f s x f'
g' : E' →L[𝕜] E''
hg' :
  HasFDerivWithinAt
    ((↑I'' : H'' → E'') ∘
      ((↑(chartAt H'' (g (f x))) : M'' → H'') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M')) ∘
        (↑I'.symm : E' → H'))
    g'
    ((↑I'.symm : E' → H') ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H' (f x))) : H' → M') ⁻¹' u ∩
      range (↑I' : H' → E'))
    ((↑I' : H' → E') ((↑(chartAt H' (f x)) : M' → H') (f x)))
G : HasMFDerivWithinAt I' I'' g u (f x) g'
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact (HasMFDerivWithinAt.comp x G F h).mdifferentiableWithinAt

Premises used: HasMFDerivWithinAt.mdifferentiableWithinAt, 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'
y : M'
hg : MDifferentiableWithinAt I' I'' g u y
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hy : f x = y
⊢ MDifferentiableWithinAt I' I'' g u (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''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
hg.comp _ hf h

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''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : s ⊆ f ⁻¹' u
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact hg.comp _ hf h

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''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
(hg.comp _ (hf.mono inter_subset_right) inter_subset_left).mono_of_mem_nhdsWithin
    (Filter.inter_mem h self_mem_nhdsWithin)

Premises used: Filter.inter_mem, Set.inter_subset_left, MDifferentiableWithinAt.mono, self_mem_nhdsWithin, MDifferentiableWithinAt.comp, MDifferentiableWithinAt.mono_of_mem_nhdsWithin, 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'
y : M'
hg : MDifferentiableWithinAt I' I'' g u y
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hy : f x = y
⊢ MDifferentiableWithinAt I' I'' g u (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''
u : Set M'
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin _ hg hf h

Premises used: MDifferentiableWithinAt.comp_of_preimage_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'
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hg : MDifferentiableWithinAt I' I'' g u (f x)
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x

Tactic:
exact MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin _ hg hf h

Premises used: MDifferentiableWithinAt.comp_of_preimage_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
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I'' (g ∘ f) x

Tactic:
(hg.hasMFDerivAt.comp x hf.hasMFDerivAt).mdifferentiableAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt, HasMFDerivAt.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
g : M' → M''
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableAt I I' f 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
g : M' → M''
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ MDifferentiableAt I I'' (g ∘ f) x

Tactic:
hg.comp _ hf

Premises used: MDifferentiableAt.comp