awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
Tactic: have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
    (isOpen_extChartAt_source x).uniqueMDiffWithinAt h'y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
have rw : MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
Tactic: rw [mfderivWithin_eq_mfderiv U']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have this : Eq (α :=
  TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
  (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
  (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
Tactic: have : mfderiv% (extChartAt I x) ((extChartAt I x).symm y)
      = mfderiv[(extChartAt I x).source] (extChartAt I x) ((extChartAt I x).symm y) := by
    rw [mfderivWithin_eq_mfderiv U']
    exact mdifferentiableAt_extChartAt h''y
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have rw : Eq (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
  (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
      ((↑(extChartAt I x).symm : E → M) y) :
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace I
        (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
Tactic: rw [this, ← mfderivWithin_comp_of_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
rw :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
Tactic: rw [this, ← mfderivWithin_comp_of_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
rw :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have hf : MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
Tactic: rw [this, ← mfderivWithin_comp_of_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
rw :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
hf : MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have h : (extChartAt I x).source ⊆ (↑(extChartAt I x) : M → E) ⁻¹' range (↑I : H → E)
Tactic: rw [this, ← mfderivWithin_comp_of_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
rw :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
hf : MDiffAt[(extChartAt I x).source] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
h : (extChartAt I x).source ⊆ (↑(extChartAt I x) : M → E) ⁻¹' range (↑I : H → E)
hxs : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(𝕜, E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y)
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have hy₁ : (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) = y
Tactic: rw [this, ← mfderivWithin_comp_of_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
z : M
hz : z ∈ (extChartAt I x).source
⊢ z ∈ (↑(extChartAt I x) : M → E) ⁻¹' range (↑I : H → E)
have h : (↑(extChartAt I x) : M → E) z ∈ (extChartAt I x).target
Tactic: apply extChartAt_target_subset_range x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I ((↑(extChartAt I x).symm : E → M) y)))
have rw : Eq (α := TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
  (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
      ((↑(extChartAt I x).symm : E → M) y) :
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace I
        (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
  (mfderivWithin I I id (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
Tactic: rw [← mfderivWithin_id U']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin I I id (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
have hL : (↑(extChartAt I x).symm : E → M) ∘
    (↑(extChartAt I x) : M → E) =ᶠ[𝓝[(extChartAt I x).source] (↑(extChartAt I x).symm : E → M) y]
  id
Tactic: apply Filter.EventuallyEq.mfderivWithin_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
hL :
  (↑(extChartAt I x).symm : E → M) ∘
      (↑(extChartAt I x) : M → E) =ᶠ[𝓝[(extChartAt I x).source] (↑(extChartAt I x).symm : E → M) y]
    id
⊢ Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I I ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) (extChartAt I x).source
        ((↑(extChartAt I x).symm : E → M) y) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
        TangentSpace I
          (((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin I I id (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
have hx : ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) ((↑(extChartAt I x).symm : E → M) y) =
  id ((↑(extChartAt I x).symm : E → M) y)
Tactic: apply Filter.EventuallyEq.mfderivWithin_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Atlas (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
inst_6 : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y)
this :
  Eq (α :=
    TangentSpace I ((↑(extChartAt I x).symm : E → M) y) →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
    (mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x) : M → E) (extChartAt I x).source ((↑(extChartAt I x).symm : E → M) y))
⊢ (↑(extChartAt I x).symm : E → M) ∘
      (↑(extChartAt I x) : M → E) =ᶠ[𝓝[(extChartAt I x).source] (↑(extChartAt I x).symm : E → M) y]
    id
have h : ∀ (z : M) (hz : z ∈ (extChartAt I x).source), ((↑(extChartAt I x).symm : E → M) ∘ (↑(extChartAt I x) : M → E)) z = id z
Tactic: filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz