awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
have hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
Tactic: have hφ' : ContDiffOn 𝕜 n φ.symm φ.target := I.contDiffOn_extendCoordChange_symm he he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
have refine_1 : Eq (α := E →L[𝕜] E)
  (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
  (ContinuousLinearMap.id 𝕜 E)
Tactic: refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_1 :
  Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
⊢ ContinuousLinearMap.IsInvertible (fderivWithin 𝕜 (↑φ : E → E) φ.source x)
have refine_2 : Eq (α := E →L[𝕜] E)
  (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
  (ContinuousLinearMap.id 𝕜 E)
Tactic: refine .of_inverse (g := (fderivWithin 𝕜 φ.symm φ.target (φ x))) ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have refine_1 : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
Tactic: rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_1 : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have refine_1₁ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source ((↑φ.symm : E → E) ((↑φ : E → E) x))
Tactic: rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_1 : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
refine_1₁ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source ((↑φ.symm : E → E) ((↑φ : E → E) x))
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have refine_1₂ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
Tactic: rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_1 : UniqueDiffWithinAt 𝕜 φ.target ((↑φ : E → E) x)
refine_1₁ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source ((↑φ.symm : E → E) ((↑φ : E → E) x))
refine_1₂ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ : E → E) φ.source x ∘SL fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x))
    (ContinuousLinearMap.id 𝕜 E)
have refine_1₃ : MapsTo (↑φ.symm : E → E) φ.target φ.source
Tactic: rw [← φ.left_inv hx, φ.right_inv (φ.map_source hx), ← fderivWithin_comp,
      fderivWithin_congr' φ.rightInvOn.eqOn (φ.map_source hx), fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)
have refine_2 : UniqueDiffWithinAt 𝕜 φ.source x
Tactic: rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_2 : UniqueDiffWithinAt 𝕜 φ.source x
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)
have refine_2₁ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
Tactic: rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_2 : UniqueDiffWithinAt 𝕜 φ.source x
refine_2₁ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)
have refine_2₂ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source x
Tactic: rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst_5 : ChartedSpace H M
hn : n ≠ 0
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e'
x : E
φ : PartialEquiv E E := extendCoordChange.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (I := I) e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ : E → E) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm : E → E) φ.target
refine_2 : UniqueDiffWithinAt 𝕜 φ.source x
refine_2₁ : DifferentiableWithinAt 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x)
refine_2₂ : DifferentiableWithinAt 𝕜 (↑φ : E → E) φ.source x
⊢ Eq (α := E →L[𝕜] E)
    (fderivWithin 𝕜 (↑φ.symm : E → E) φ.target ((↑φ : E → E) x) ∘SL fderivWithin 𝕜 (↑φ : E → E) φ.source x)
    (ContinuousLinearMap.id 𝕜 E)
have refine_2₃ : MapsTo (↑φ : E → E) φ.source φ.target
Tactic: rw [← fderivWithin_comp, fderivWithin_congr' φ.leftInvOn.eqOn hx, fderivWithin_id]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (extChartAt I x).target
have rw : UniqueDiffOn 𝕜 ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target ∩ range (↑I : H → E))
Tactic: rw [extChartAt_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
⊢ map (↑(extChartAt I x) : M → E) (𝓝 x) = 𝓝 ((↑(extChartAt I x) : M → E) x)
have rw : map (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) (𝓝 x) =
  𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)
Tactic: rw [extChartAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : (↑(extChartAt I x) : M → E) y ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 y
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) y)
have rw : (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
  𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) y)
Tactic: rw [extChartAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
have rw : (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
  𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)
Tactic: rw [extChartAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] y
have rw : (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
Tactic: rw [← (extChartAt I x).right_inv hy]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
have hy₁ : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
Tactic: apply extChartAt_target_mem_nhdsWithin'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 y
have rw : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝[range (↑I : H → E)] y ⊔ 𝓝[(range (↑I : H → E))ᶜ] y
Tactic: rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (extChartAt I x).target
have simp_rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target)
Tactic: simp_rw [extChartAt_target, I.range_eq_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
inst_6 : I.Boundaryless
x : M
⊢ (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
have h : 𝓝 ((↑(extChartAt I x) : M → E) x) = 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: convert! extChartAt_target_mem_nhdsWithin x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] z = 𝓝[range (↑I : H → E)] z
have rw : 𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z) =
  𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z)
Tactic: rw [← PartialEquiv.right_inv (extChartAt I x) hz]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)
have rw : ∀ t ∈ 𝓝 y, (t ∩ interior (extChartAt I x).target).Nonempty
Tactic: rw [mem_closure_iff_nhds]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty
have A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
Tactic: have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
    inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem hy)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty
have B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
Tactic: have B : y ∈ closure (interior (range I)) := by
    apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
⊢ (t ∩ interior (extChartAt I x).target).Nonempty
have obtain : ∀ (z : E) (hz : z ∈ interior (range (↑I : H → E))) (tz : z ∈ t)
  (h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ), (t ∩ interior (extChartAt I x).target).Nonempty
Tactic: obtain ⟨z, ⟨tz, h'z⟩, hz⟩ :
      (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
    mem_closure_iff_nhds.1 B _ A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
⊢ (t ∩ interior (extChartAt I x).target).Nonempty
have refine : z ∈ interior (extChartAt I x).target
Tactic: refine ⟨z, ⟨tz, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
⊢ z ∈ interior (extChartAt I x).target
have h''z : z ∈ (extChartAt I x).target
Tactic: have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
⊢ (interior (extChartAt I x).target).Nonempty
have by_contra! : ∀ (H : interior (extChartAt I x).target = ∅), False
Tactic: by_contra! H