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_1 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H_1
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H_1
inst_5 : ChartedSpace H_1 M
x : M
H : interior (extChartAt I x).target = ∅
⊢ False
have this : (↑(extChartAt I x) : M → E) x ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)
Tactic: have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) 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
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ (↑(extChartAt I x₀) : M → E) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target))
have simp_rw : ∀ (o : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
    (↑(extChartAt I x₀) : M → E) x ∈ o →
      (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
Tactic: simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]
-- 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
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
⊢ ((↑(extChartAt I x₀) : M → E) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty
have this : (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x
Tactic: have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
-- 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
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
this : (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x
⊢ ((↑(extChartAt I x₀) : M → E) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty
have refine : (extChartAt I x₀).source ∈ 𝓝 x
Tactic: refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
-- 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
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
have obtain : ∀ (y : M) (ys : y ∈ interior s) (yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o) (hy : y ∈ (extChartAt I x₀).source),
  (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
Tactic: obtain ⟨y, ⟨yo, hy⟩, ys⟩ :
      ((extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty := by
    have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
    refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
    apply (isOpen_extChartAt_source x₀).mem_nhds h'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
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
have simp : (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
Tactic: simp only [interior_mem_nhds]
-- 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
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
have apply : s ∈ 𝓝 ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) y))
Tactic: apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
-- 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
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) y))
have simp : s ∈ 𝓝 y
Tactic: simp only [hy, PartialEquiv.left_inv]
-- 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
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
have A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
Tactic: have A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (extChartAt I x₀ y) := by
    simp only [interior_mem_nhds]
    apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
    simp only [hy, PartialEquiv.left_inv]
    exact mem_interior_iff_mem_nhds.mp ys
-- 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
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ (↑(extChartAt I x₀) : M → E) y ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)
have a : (↑(extChartAt I x₀) : M → E) y ∈ (extChartAt I x₀).target
Tactic: apply extChartAt_target_subset_closure_interior (x := x₀)
-- 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
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
have B : (↑(extChartAt I x₀) : M → E) y ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)
Tactic: have B : (extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target) := by
    apply extChartAt_target_subset_closure_interior (x := x₀)
    exact (extChartAt I x₀).map_source 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((toPartialEquiv (chartAt H x)).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)
have rw : IsOpen[inst_4] ((extChartAt I x).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)
Tactic: rw [← extChartAt_source I]
-- 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 t : Set M
inst_5 : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝[s] x'
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
have rwa : ∀
  (ht :
    t ∈
      map (↑(extChartAt I x).symm : E → M)
        (𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x')),
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
Tactic: rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht
Cleared hypotheses: ht
-- 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 t : Set M
inst_5 : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝[s] x'
rwa :
  ∀
    (ht :
      t ∈
        map (↑(extChartAt I x).symm : E → M)
          (𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x')),
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
have rwa₁ : ∀
  (ht :
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
      𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'),
  (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x'
Tactic: rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht
Cleared hypotheses: ht
-- 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
t : Set M
inst_5 : ChartedSpace H M
x : M
ht : t ∈ 𝓝 x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' t ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
have apply : t ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
Tactic: apply (continuousAt_extChartAt_symm x).preimage_mem_nhds
-- 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 t : Set M
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) =
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t
have h : ∀ (x_1 : E),
  x_1 ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E) ↔
    x_1 ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t
Tactic: mfld_set_tac
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
    𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
      (↑(extChartAt I x) : M → E) x
have rw : f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x
Tactic: rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image,
    ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
f : M → M'
x : M
hc : ContinuousWithinAt f s x
⊢ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(extChartAt I x) : M → E) x)]
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
have rw : 𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x =
  𝓝[(extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)]
    (↑(extChartAt I x) : M → E) x
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq]
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace N
inst_17 : TopologicalSpace G'
inst_18 : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst_19 : ChartedSpace G N
inst_20 : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
⊢ writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)
have h : ∀ (p : E × E'),
  (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1
Tactic: ext p
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace N
inst_17 : TopologicalSpace G'
inst_18 : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst_19 : ChartedSpace G N
inst_20 : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
h :
  ∀ (p : E × E'),
    (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).1 =
      (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).1
⊢ writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)
have h₁ : ∀ (p : E × E'),
  (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).2 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).2
Tactic: ext p
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M × M'
⊢ extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)
have simp : (toPartialEquiv (chartAt H x.1)).prod (toPartialEquiv (chartAt H' x.2)) ≫ I.prod I'.toPartialEquiv =
  (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)
Tactic: simp only [mfld_simps]
-- 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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M × M'
⊢ (toPartialEquiv (chartAt H x.1)).prod (toPartialEquiv (chartAt H' x.2)) ≫ I.prod I'.toPartialEquiv =
    (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)
have rw : (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv) =
  (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)
Tactic: rw [PartialEquiv.prod_trans]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
⊢ LocallyCompactSpace M
have this : ProperSpace E
Tactic: have : ProperSpace E := FiniteDimensional.proper 𝕜 E
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
this : ProperSpace E
⊢ LocallyCompactSpace M
have this₁ : LocallyCompactSpace H
Tactic: have : LocallyCompactSpace H := I.locallyCompactSpace
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
h : Nonempty M
inst_6 : LocallyCompactSpace M
⊢ LocallyCompactSpace E
have rcases : ∀ (x : M), LocallyCompactSpace E
Tactic: rcases h with ⟨x⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
⊢ LocallyCompactSpace E
have obtain : ∀ (y : E) (hy : y ∈ interior (extChartAt I x).target), LocallyCompactSpace E
Tactic: obtain ⟨y, hy⟩ := interior_extChartAt_target_nonempty I x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (hypothesis)
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
⊢ LocallyCompactSpace E
have h'y : y ∈ (extChartAt I x).target
Tactic: have h'y : y ∈ (extChartAt I x).target := interior_subset hy