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'
g : M' → M''
x : M
hf : MDifferentiableAt I I' f x
hg : MDifferentiableAt I' I'' g (f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x)))
    (mfderiv I I'' (g ∘ f) x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderiv I' I'' g (f x)) (mfderiv I I' f x))

Tactic:
exact mfderiv_comp x hg hf

Premises used: mfderiv_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''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
rw :
  Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderiv I' I'' g (f x)) (mfderiv I I' f x) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g (f x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
              (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g (f x)))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I I'' (g ∘ f) x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g (f x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
              (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g (f x)))

Tactic:
rw [mfderiv_comp _ hg hf]

Premises used: mfderiv_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''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderiv I' I'' g (f x)) (mfderiv I I' f x) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g (f x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
              (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g (f x)))

Tactic:
rfl
-- 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
v : TangentSpace I x
subst :
  ∀ (hg : MDifferentiableAt I' I'' g (f x)),
    Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
      (((mfderiv I I'' (g ∘ f) x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace I'' ((g ∘ f) x))) :
            (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
          v :
        TangentSpace I'' ((g ∘ f) x))
      (((mfderiv I' I'' g (f x) :
              ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
                (TangentSpace I'' (g (f x)))) :
            (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
          (((mfderiv I I' f x :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
              (a : TangentSpace I x) → TangentSpace I' (f x))
            v) :
        TangentSpace I'' (g (f x)))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I I'' (g ∘ f) x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g y :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' y) (TangentSpace I'' (g y))) :
          (a : TangentSpace I' y) → TangentSpace I'' (g y))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g y))

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
v : TangentSpace I x
hg : MDifferentiableAt I' I'' g (f x)
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I I'' (g ∘ f) x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g (f x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
              (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g (f x)))

Tactic:
mfderiv_comp_apply _ hg hf v

Premises used: mfderiv_comp_apply
-- 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
v : TangentSpace I x
hg : MDifferentiableAt I' I'' g (f x)
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I I'' (g ∘ f) x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I'' ((g ∘ f) x))) :
          (a : TangentSpace I x) → TangentSpace I'' ((g ∘ f) x))
        v :
      TangentSpace I'' ((g ∘ f) x))
    (((mfderiv I' I'' g (f x) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f x))
              (TangentSpace I'' (g (f x)))) :
          (a : TangentSpace I' (f x)) → TangentSpace I'' (g (f x)))
        (((mfderiv I I' f x :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
            (a : TangentSpace I x) → TangentSpace I' (f x))
          v) :
      TangentSpace I'' (g (f x)))

Tactic:
exact mfderiv_comp_apply _ hg hf v

Premises used: mfderiv_comp_apply
-- 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'
hg : MDifferentiableOn I' I'' g u
hf : MDifferentiableOn I I' f s
st : s ⊆ f ⁻¹' u
⊢ MDifferentiableOn I I'' (g ∘ f) s

Tactic:
fun x hx =>
  MDifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

Premises used: MDifferentiableOn, 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'
s : Set M
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiableOn I I' f s
⊢ MDifferentiableOn I' I'' g univ

Tactic:
rw [← mdifferentiableOn_univ] at hg

Premises used: mdifferentiableOn_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'
s : Set M
g : M' → M''
hg : MDifferentiable I' I'' g
hf : MDifferentiableOn I I' f s
hg₁ : MDifferentiableOn I' I'' g univ
⊢ MDifferentiableOn I I' f s

Tactic:
rw [← mdifferentiableOn_univ] at hg

Premises used: mdifferentiableOn_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'
s : Set M
g : M' → M''
hg : MDifferentiableOn I' I'' g univ
hf : MDifferentiableOn I I' f s
⊢ 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'
s : Set M
g : M' → M''
hg : MDifferentiableOn I' I'' g univ
hf : MDifferentiableOn I I' f s
⊢ MDifferentiableOn I I'' (g ∘ f) s

Tactic:
exact hg.comp hf (by simp)

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

Tactic:
fun x => MDifferentiableAt.comp x (hg (f x)) (hf x)

Premises used: MDifferentiableAt.comp, MDifferentiable
-- 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'
p : TangentBundle I M
hg : MDifferentiableWithinAt I' I'' g u (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableWithinAt I I' f s (p.proj (E := TangentSpace I))
h : s ⊆ f ⁻¹' u
hps : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
simp :
  Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderivWithin I I'' (g ∘ f) s (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I'' ((g ∘ f) (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderivWithin I' I'' g u (f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
⊢ Eq (α := TangentBundle I'' M'') (tangentMapWithin I I'' (g ∘ f) s p)
    (tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p))

Tactic:
simp only [tangentMapWithin, mfld_simps]

Premises used: tangentMapWithin
-- 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'
p : TangentBundle I M
hg : MDifferentiableWithinAt I' I'' g u (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableWithinAt I I' f s (p.proj (E := TangentSpace I))
h : s ⊆ f ⁻¹' u
hps : UniqueMDiffWithinAt I s (p.proj (E := TangentSpace I))
⊢ Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (mfderivWithin I' I'' g u (f (p.proj (E := TangentSpace I))))
              (mfderivWithin I I' f s (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I p.proj) → TangentSpace I'' (g (f p.proj)))
        (p.snd (E := TangentSpace I)) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
    (((mfderivWithin I' I'' g u (f (p.proj (E := TangentSpace I))) :
            ContinuousLinearMap.{u_1, u_1, u_5, u_8} (RingHom.id 𝕜) (TangentSpace I' (f (p.proj (E := TangentSpace I))))
              (TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))) :
          (a : TangentSpace I' (f p.proj)) → TangentSpace I'' (g (f p.proj)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))) :
      TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))

Tactic:
rfl