awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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 : HasMFDerivAt I' I'' g (f x) g'
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I'' (g ∘ f) s x (g' ∘SL f')
have hg₁ : HasMFDerivWithinAt I' I'' g univ (f x) g'
Tactic: rw [← hasMFDerivWithinAt_univ] at *
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'
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
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
have 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
Tactic: rcases hf.2 with ⟨f', hf'⟩
-- 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'
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))
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
have F : HasMFDerivWithinAt I I' f s x f'
Tactic: have F : HasMFDerivWithinAt I I' f s x f' := ⟨hf.1, 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
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'
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
have 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
Tactic: rcases hg.2 with ⟨g', hg'⟩
-- 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'
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)))
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s x
have G : HasMFDerivWithinAt I' I'' g u (f x) g'
Tactic: have G : HasMFDerivWithinAt I' I'' g u (f x) g' := ⟨hg.1, hg'⟩
-- 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'
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 ∘ f) s x
have hg₁ : MDifferentiableWithinAt I' I'' g u (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'
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 ∘ f) s x
have hg₁ : MDifferentiableWithinAt I' I'' g u (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'
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
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 (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'
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 ∘ f) s x
have hg₁ : MDifferentiableWithinAt I' I'' g univ (f x)
Tactic: rw [← mdifferentiableWithinAt_univ] at hg
Cleared hypotheses: hg, hf
-- 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'
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
⊢ MDifferentiableWithinAt I I'' (g ∘ f) s 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
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
⊢ 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 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))
Tactic: apply HasMFDerivWithinAt.mfderivWithin _ hxs
-- 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'
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
⊢ 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 (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'
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
⊢ 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 A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
Tactic: have A : s ∩ f ⁻¹' u ∈ 𝓝[s] x := Filter.inter_mem self_mem_nhdsWithin h
-- 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
⊢ 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)
have apply : MDifferentiableWithinAt I I'' (g ∘ f) (s ∩ f ⁻¹' u) x
Tactic: apply MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin _ hxs A
-- 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'
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)
    (ContinuousLinearMap.comp (M₂ := TangentSpace I' (f x)) (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x))
have 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)
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
-- 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'
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_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 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)
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