awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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)
C :
  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)
⊢ 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))
have rw : 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 ∩ f ⁻¹' u) x)
  (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x))
    (mfderivWithin I I' f (s ∩ f ⁻¹' u) x))
Tactic: rw [B, C]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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
hxs : UniqueMDiffWithinAt I s x
hy : f x = y
⊢ 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))
have 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))
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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
hxs : UniqueMDiffWithinAt I 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)) (mfderiv I' I'' g (f x)) (mfderivWithin I I' f s x))
have rw : 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 univ (f x))
    (mfderivWithin I I' f s x))
Tactic: rw [← mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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''
x : M
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableWithinAt I I' f s x
hxs : UniqueMDiffWithinAt I s x
hy : f x = y
⊢ 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) (mfderiv I' I'' g y) (mfderivWithin I I' f s x))
have subst : ∀ (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)))
    (mfderivWithin I I'' (g ∘ f) s x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderiv I' I'' g (f x)) (mfderivWithin I I' f s x))
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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
⊢ 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))
have h : HasMFDerivAt I I'' (g ∘ f) x
  (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderiv I' I'' g (f x)) (mfderiv I I' f x))
Tactic: apply HasMFDerivAt.mfderiv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (hypothesis)
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
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableAt I I' f x
hy : f x = y
⊢ 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))
have hg₁ : MDifferentiableAt I' I'' g (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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))
    (((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)))
have 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)))
Tactic: rw [mfderiv_comp _ hg hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (hypothesis)
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 ∘ f) s
have hg₁ : MDifferentiableOn I' I'' g univ
Tactic: rw [← mdifferentiableOn_univ] at hg
Cleared hypotheses: hg, hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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 (α := TangentBundle I'' M'') (tangentMapWithin I I'' (g ∘ f) s p)
    (tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p))
have 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)))))
Tactic: simp only [tangentMapWithin, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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''
p : TangentBundle I M
hg : MDifferentiableAt I' I'' g (f (p.proj (E := TangentSpace I)))
hf : MDifferentiableAt I I' f (p.proj (E := TangentSpace I))
⊢ Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p) (tangentMap I' I'' g (tangentMap I I' f p))
have simp : Eq.{u_8 + 1} (α := TangentSpace I'' (g (f (p.proj (E := TangentSpace I)))))
  (((mfderiv I I'' (g ∘ f) (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)))))
  (((mfderiv I' I'' g (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)))
      (((mfderiv I I' f (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: simp only [tangentMap, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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
⊢ Eq (α := TangentBundle I M → TangentBundle I'' M'') (tangentMap I I'' (g ∘ f))
    (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f))
have h : ∀ (p : TangentBundle I M),
  Eq (α := TangentBundle I'' M'') (tangentMap I I'' (g ∘ f) p)
    (Function.comp (β := TangentBundle I' M') (tangentMap I' I'' g) (tangentMap I I' f) p)
Tactic: ext p : 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
    ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
H' : Type u_6
inst_5 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
f : E → H'
s : Set E
x : E
simp_rw :
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
      ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range (↑𝓘(𝕜, E) : E → E)) ((↑𝓘(𝕜, E) : E → E) x) ↔
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
⊢ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
have simp_rw₁ : DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f ∘ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E))
    ((↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) ⁻¹' s ∩ range id) (id x) ↔
  DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ f) s x
Tactic: simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ,
    modelWithCornersSelf_coe_symm, CompTriple.comp_eq, preimage_id_eq, id_eq]