awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
rw :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₁ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
have rw₂ : 𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y
Tactic: rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
rw :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₁ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₂ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
have rw₃ : 𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
Tactic: rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
rw :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₁ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₂ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y
rw₃ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
have rw₄ : 𝓝[(f.extend I).target ∩ (↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y =
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
Tactic: rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
rw :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₁ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
rw₂ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y ⊓ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y
rw₃ :
  𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
rw₄ :
  𝓝[(f.extend I).target ∩ (↑(f.extend I).symm : E → M) ⁻¹' s] (↑(f.extend I) : M → E) y =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y
have rw₅ : 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y =
  𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ (f.extend I).target] (↑(f.extend I) : M → E) y
Tactic: rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
    inter_comm]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm : E → M)
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    𝓝[s] y
have rw : (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) =ᶠ[𝓝[s] y] id
Tactic: rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝 y
have rw : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝[univ] y
Tactic: rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
rw : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝[univ] y
⊢ map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝 y
have rw₁ : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
  map (↑(f.extend I).symm : E → M)
    (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
Tactic: rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
rw : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝[univ] y
rw₁ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M)
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
⊢ map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝 y
have rw₂ : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
  map (↑(f.extend I).symm : E → M) (𝓝[univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
Tactic: rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
rw : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝[univ] y
rw₁ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M)
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
rw₂ :
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
    map (↑(f.extend I).symm : E → M) (𝓝[univ ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
⊢ map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) = 𝓝 y
have rw₃ : map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y) =
  map (↑(f.extend I).symm : E → M) (𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y)
Tactic: rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
⊢ Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y)) ↔ Tendsto g l (𝓝 y)
have refine : ∀ (h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))) (u : Set M) (hu : u ∈ 𝓝 y), g ⁻¹' u ∈ l
Tactic: refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.comp⟩
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
⊢ g ⁻¹' u ∈ l
have this : Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l
  (𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y)))
Tactic: have := (f.continuousAt_extend_symm hy).tendsto.comp h
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
this :
  Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l
    (𝓝 ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y)))
⊢ g ⁻¹' u ∈ l
have this₁ : Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l (𝓝 y)
Tactic: rw [extend_left_inv _ hy] at this
Cleared hypotheses: 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
α : Type u_8
l : Filter α
g : α → M
hg : ∀ᶠ (z : α) in l, g z ∈ f.source
y : M
hy : y ∈ f.source
h : Tendsto ((↑(f.extend I) : M → E) ∘ g) l (𝓝 ((↑(f.extend I) : M → E) y))
u : Set M
hu : u ∈ 𝓝 y
this : Tendsto ((↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g) l (𝓝 y)
⊢ g ⁻¹' u ∈ l
have h₁ : ∀ (z : α) (hz : g z ∈ f.source) (hzu : z ∈ (↑(f.extend I).symm : E → M) ∘ (↑(f.extend I) : M → E) ∘ g ⁻¹' u),
  z ∈ g ⁻¹' u
Tactic: filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
      (𝓝 (((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) y))) ↔
    Tendsto g (𝓝[s] y) (𝓝 (g y))
have simp : Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
    (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
    (𝓝 ((↑(f'.extend I') : M' → E') (g ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y))))) ↔
  Tendsto g (𝓝[s] y) (𝓝 (g y))
Tactic: simp only [comp_apply]
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ Tendsto ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M))
      (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y)
      (𝓝 ((↑(f'.extend I') : M' → E') (g ((↑(f.extend I).symm : E → M) ((↑(f.extend I) : M → E) y))))) ↔
    Tendsto g (𝓝[s] y) (𝓝 (g y))
have rw : ∀ᶠ (z : E) in 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y,
  (g ∘ (↑(f.extend I).symm : E → M)) z ∈ f'.source
Tactic: rw [extend_left_inv _ hy, f'.tendsto_extend_comp_iff _ hgy,
    ← f.map_extend_symm_nhdsWithin (I := I) hy, tendsto_map'_iff]
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ ∀ᶠ (z : E) in 𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) y,
    (g ∘ (↑(f.extend I).symm : E → M)) z ∈ f'.source
have rw : ∀ᶠ (a : M) in 𝓝[s] y, (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) a) ∈ f'.source
Tactic: rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
⊢ ∀ᶠ (a : M) in 𝓝[s] y, (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) a) ∈ f'.source
have h : ∀ (z : M) (hz : z ∈ s ∩ f.source), (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) z) ∈ f'.source
Tactic: filter_upwards [inter_mem_nhdsWithin _ (f.open_source.mem_nhds hy)] with z 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
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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) z) ∈ f'.source
have h : g z ∈ f'.source
Tactic: rw [comp_apply, extend_left_inv _ hz.2]
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
⊢ ContinuousOn ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s) ↔
    ContinuousOn g s
have refine : ∀ (x : M) (hx : x ∈ s),
  ContinuousWithinAt ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s)
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt g s x
Tactic: refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ ContinuousWithinAt ((↑(f'.extend I') : M' → E') ∘ g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I) : M → E) '' s)
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt g s x
have refine : (↑(f.extend I) : M → E) '' s =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
Tactic: refine (continuousWithinAt_congr_set ?_).trans
    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)
-- 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
f : OpenPartialHomeomorph M H
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
f' : OpenPartialHomeomorph M' H'
g : M → M'
hs : s ⊆ f.source
hmaps : MapsTo g s f'.source
x : M
hx : x ∈ s
⊢ (↑(f.extend I) : M → E) '' s =ᶠ[𝓝 ((↑(f.extend I) : M → E) x)] (↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
have hy : x ∈ f.source
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin_eq_image_of_subset,
    ← map_extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
x : M
hx : x ∈ f.source
hs : s ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
⊢ (↑(f.extend I) : M → E) ⁻¹' s ∈ 𝓝 x
have rwa : ∀ (hs : s ∈ map (↑(f.extend I) : M → E) (𝓝 x)), (↑(f.extend I) : M → E) ⁻¹' s ∈ 𝓝 x
Tactic: rwa [← map_extend_nhds (I := I) f hx] at hs
Cleared hypotheses: hs
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s t : Set M
x : M
h : x ∈ f.source
ht : t ∈ 𝓝[s] x
⊢ (↑(f.extend I).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa : ∀
  (ht :
    t ∈
      map (↑(f.extend I).symm : E → M)
        (𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x)),
  (↑(f.extend I).symm : E → M) ⁻¹' t ∈
    𝓝[(↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(f.extend I) : M → E) x
Tactic: rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht
Cleared hypotheses: ht