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
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
rw₁ : (↑I.toPartialEquiv : H → E) '' (I.source ∩ f.target) = (↑I : H → E) '' f.target
rw₂ : (↑I.toPartialEquiv : H → E) '' (univ ∩ f.target) = (↑I : H → E) '' f.target
rw₃ : (↑I.toPartialEquiv : H → E) '' f.target = (↑I : H → E) '' f.target
⊢ (f.extend I).target = (↑I : H → E) '' f.target
have rw₄ : (↑I : H → E) '' f.target = (↑I : H → E) '' f.target
Tactic: rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]
-- 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
⊢ (f.extend I).target = (↑(f.extend I) : M → E) '' f.source
have rw : (↑I : H → E) '' f.target = (↑(f.extend I) : M → E) '' f.source
Tactic: rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]
-- 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
rw : (↑I : H → E) '' f.target = (↑(f.extend I) : M → E) '' f.source
⊢ (f.extend I).target = (↑(f.extend I) : M → E) '' f.source
have rw₁ : (↑I : H → E) '' (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
Tactic: rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]
-- 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
rw : (↑I : H → E) '' f.target = (↑(f.extend I) : M → E) '' f.source
rw₁ : (↑I : H → E) '' (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
⊢ (f.extend I).target = (↑(f.extend I) : M → E) '' f.source
have rw₂ : (↑I : H → E) ∘ (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
Tactic: rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]
-- 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
rw : (↑I : H → E) '' f.target = (↑(f.extend I) : M → E) '' f.source
rw₁ : (↑I : H → E) '' (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
rw₂ : (↑I : H → E) ∘ (↑f : M → H) '' f.source = (↑(f.extend I) : M → E) '' f.source
⊢ (f.extend I).target = (↑(f.extend I) : M → E) '' f.source
have rw₃ : (↑I : H → E) ∘ (↑f : M → H) '' f.source = (↑I : H → E) ∘ (↑f : M → H) '' f.source
Tactic: rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]
-- 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
inst_5 : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.extend I).target
have rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' f.target)
Tactic: rw [extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ MapsTo (↑(f.extend I) : M → E) s ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
have rw : (↑I : H → E) '' (f.target ∩ (↑f.symm : H → M) ⁻¹' s) ⊆ (↑I : H → E) '' (↑f.symm : H → M) ⁻¹' s
Tactic: rw [mapsTo_iff_image_subset, extend_coe, extend_coe_symm, preimage_comp, ← I.image_eq, image_comp,
    f.image_eq_target_inter_inv_preimage 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
⊢ ContinuousOn (↑(f.extend I) : M → E) (f.extend I).source
have refine : ContinuousOn (↑(f.symm.restr I.source).symm : M → H) (f.extend I).source
Tactic: refine I.continuous.comp_continuousOn ?_
-- 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
⊢ ContinuousOn (↑(f.symm.restr I.source).symm : M → H) (f.extend I).source
have rw : ContinuousOn (↑(f.symm.restr I.source).symm : M → H) f.source
Tactic: rw [extend_source]
-- 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
x : M
hy : x ∈ f.source
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
Tactic: rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_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
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
x : M
hy : x ∈ f.source
rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa₁ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑f : M → H) x)
Tactic: rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_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
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
x : M
hy : x ∈ f.source
rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
rwa₁ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑f : M → H) x)
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa₂ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (𝓝 ((↑f : M → H) x))
Tactic: rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_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
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
x : M
hy : x ∈ f.source
rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
rwa₁ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑f : M → H) x)
rwa₂ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (𝓝 ((↑f : M → H) x))
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa₃ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (map (↑f : M → H) (𝓝 x))
Tactic: rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_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
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
x : M
hy : x ∈ f.source
rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
rwa₁ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑f : M → H) x)
rwa₂ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (𝓝 ((↑f : M → H) x))
rwa₃ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (map (↑f : M → H) (𝓝 x))
rwa₄ : x ∈ f.source
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rwa₅ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x)
Tactic: rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_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
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
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)
have rw : range (↑I : H → E) ∈ 𝓝 ((↑(f.extend I) : M → E) x)
Tactic: rw [f.map_extend_nhds hx, nhdsWithin_eq_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)
have rw : 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
Tactic: rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
rw : 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)
have rw₁ : 𝓝[univ] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
Tactic: rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
rw : 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
rw₁ : 𝓝[univ] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)
have rw₂ : 𝓝 ((↑(f.extend I) : M → E) x) = 𝓝 ((↑(f.extend I) : M → E) x)
Tactic: rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ (f.extend I).target ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y
have rw : (↑(f.extend I) : M → E) '' (f.extend I).source ∈ map (↑(f.extend I) : M → E) (𝓝 y)
Tactic: rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ (↑I : H → E) '' f.target ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x
have rw : (↑f : M → H) ⁻¹' f.target ∈ 𝓝 x
Tactic: rw [← f.map_extend_nhds hx, Filter.mem_map,
    f.extend_coe, Set.preimage_comp, I.preimage_image f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) '' s ∈ 𝓝 ((↑(f.extend I) : M → E) x)
have rw : (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
Tactic: rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_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
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 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
have h₁ : ∀ (a : M), Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
Tactic: filter_upwards [h] using subset_preimage_image (f.extend I) s
-- 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
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
h₁ :
  ∀ (a : M),
    Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
have h₂ : ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s
Tactic: filter_upwards [h] using subset_preimage_image (f.extend I) s
-- 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
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) '' s ∈ 𝓝 ((↑(f.extend I) : M → E) x)
have rw : (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
Tactic: rw [← f.map_extend_nhds_of_mem_interior_range hx h'x, Filter.mem_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
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
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
have h₁ : ∀ (a : M), Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
Tactic: filter_upwards [h] using subset_preimage_image (f.extend I) s
-- 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
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
h₁ :
  ∀ (a : M),
    Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
have h₂ : ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s
Tactic: filter_upwards [h] using subset_preimage_image (f.extend I) s
-- 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
⊢ interior (f.extend I).target ⊆ interior (range (↑I : H → E))
have rw : (↑I.symm : E → H) ⁻¹' f.target ∩ interior (range (↑I : H → E)) ⊆ interior (range (↑I : H → E))
Tactic: rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq]
-- 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 : H
hy : y ∈ f.target
hy' : (↑I : H → E) y ∈ interior (range (↑I : H → E))
⊢ (↑I : H → E) y ∈ interior (f.extend I).target
have rw : (↑I.symm : E → H) ((↑I : H → E) y) ∈ f.target ∧ (↑I : H → E) y ∈ interior (range (↑I : H → E))
Tactic: rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
    mem_inter_iff, mem_preimage]
-- 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
X : Type u_8
inst_5 : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt (g ∘ (↑f.symm : H → M)) ((↑f.symm : H → M) ⁻¹' s) ((↑f : M → H) x)
have rw : ContinuousWithinAt (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(f.extend I) : M → E) x) ↔
  ContinuousWithinAt ((g ∘ (↑f.symm : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (↑f.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑f : M → H) x))
Tactic: rw [← I.symm_continuousWithinAt_comp_right_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
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
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] (f.source ∩ (↑(f.extend I) : M → E) ⁻¹' s)
have rw : IsOpen[inst_4] ((f.extend I).source ∩ (↑(f.extend I) : M → E) ⁻¹' s)
Tactic: rw [← extend_source f (I := 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
hs : s ⊆ f.source
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) = 𝓝[(↑(f.extend I) : M → E) '' s] (↑(f.extend I) : M → E) y
have rw : s ⊆ (f.extend I).source
Tactic: rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]
-- 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) : 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 ∩ range (↑I : H → E)] (↑(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
⊢ 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 ⊓ 𝓝[range (↑I : H → E)] (↑(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]