awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
⊢ MDifferentiable I I'' (e ≫ₕ e')
have left : MDiff[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'')
Tactic: constructor
-- 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
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''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
left : MDiff[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'')
⊢ MDifferentiable I I'' (e ≫ₕ e')
have right : MDiff[(e ≫ₕ e').target] (↑(e ≫ₕ e').symm : M'' → M)
Tactic: constructor
-- 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
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''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M
hx : x ∈ (e ≫ₕ e').source
⊢ MDiffAt[(e ≫ₕ e').source] (↑(e ≫ₕ e') : M → M'') x
have hx₁ : x ∈ e.source ∧ (↑e : M → M') x ∈ e'.source
Tactic: simp only [mfld_simps] at hx
Cleared hypotheses: hx
-- 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
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''
e : OpenPartialHomeomorph M M'
he : MDifferentiable I I' e
e' : OpenPartialHomeomorph M' M''
he' : MDifferentiable I' I'' e'
x : M''
hx : x ∈ (e ≫ₕ e').target
⊢ MDiffAt[(e ≫ₕ e').target] (↑(e ≫ₕ e').symm : M'' → M) x
have hx₁ : x ∈ e'.target ∧ (↑e'.symm : M'' → M') x ∈ e.target
Tactic: simp only [mfld_simps] at hx
Cleared hypotheses: hx
-- 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
z : E
h : z ∈ (extChartAt I x).target
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) z
have Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
Tactic: have Z := I.mdifferentiableWithinAt_symm (extChartAt_target_subset_range x h)
-- 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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) z
have apply : MDiffAt (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2 ((↑I.symm : E → H) z)
Tactic: apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I) _ _ Z
-- 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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
⊢ MDiffAt (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2 ((↑I.symm : E → H) z)
have apply : Membership.mem (γ := Set H) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (ChartedSpace.chartAt x)))
  ((↑I.symm : E → H) z)
Tactic: apply mdifferentiableAt_atlas_symm (ChartedSpace.chart_mem_atlas x)
-- 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
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range (↑I : H → E)] (↑I.symm : E → H) z
⊢ Membership.mem (γ := Set H) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (ChartedSpace.chartAt x)))
    ((↑I.symm : E → H) z)
have h₁ : (∃ (y : H), (↑I : H → E) y = z) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target
Tactic: simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.trans_target,
    ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm, mem_inter_iff, mem_range,
    mem_preimage] at h
Cleared hypotheses: h
-- 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
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
have a : y ∈ range (↑I : H → E)
Tactic: apply I.uniqueMDiffOn
-- 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
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
Tactic: have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y := by
    apply I.uniqueMDiffOn
    exact extChartAt_target_subset_range x hy
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
Tactic: have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
h'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have h''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
    rwa [← extChartAt_source (I := I)]
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have rw : Eq (α :=
  TangentSpace 𝓘(𝕜, E) y →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
  (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    y)
  (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
Tactic: rw [← mfderiv_comp_mfderivWithin]
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
rw :
  Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have hg : MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
Tactic: rw [← mfderiv_comp_mfderivWithin]
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
rw :
  Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
hg : MDiffAt (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderiv% (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have hf : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) y
Tactic: rw [← mfderiv_comp_mfderivWithin]
-- 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y))
have rw : Eq (α :=
  TangentSpace 𝓘(𝕜, E) y →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
  (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    y)
  (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) id (range (↑I : H → E)) 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) id (range (↑I : H → E)) y)
have hL : (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
hL : (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] y] id
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) y →L[𝕜]
      TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)))
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      y)
    (mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E) id (range (↑I : H → E)) y)
have hx : ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = id 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range (↑I : H → E)) y
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
⊢ (↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M) =ᶠ[𝓝[range (↑I : H → E)] y] id
have h : ∀ (z : E) (hz : z ∈ (extChartAt I x).target), ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) z = id z
Tactic: filter_upwards [extChartAt_target_mem_nhdsWithin_of_mem hy] with z hz
-- 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 y : M
hy : y ∈ (extChartAt I x).source
⊢ Eq (α :=
    TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y) →L[𝕜] TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I y) (mfderiv% (↑(extChartAt I x) : M → E) y)
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I x) : M → E) y)))
have this : y = (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)
Tactic: have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
-- 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
⊢ 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'y : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
Tactic: have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
-- 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
⊢ 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''y : (↑(extChartAt I x).symm : E → M) y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
Tactic: have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
    rwa [← extChartAt_source (I := I)]