awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
G : Type u_1
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiff I 𝓘(ℝ, G) (M' := G) ∞ fun (x : M) ↦ (↑f : M → ℝ) x • g x
have refine : ∀ (x : M) (hx : Membership.mem (γ := Set M) (tsupport.{uM, u_1} (α := G) fun (x : M) ↦ (↑f : M → ℝ) x • g x) x),
  ContMDiffAt I 𝓘(ℝ, G) (M' := G) ∞ (fun (x : M) ↦ (↑f : M → ℝ) x • g x) x
Tactic: refine contMDiff_of_tsupport fun x hx => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (hypothesis)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
inst_6 : T2Space M
inst_7 : IsManifold I ∞ M
G : Type u_1
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
x : M
hx : Membership.mem (γ := Set M) (tsupport.{uM, u_1} (α := G) fun (x : M) ↦ (↑f : M → ℝ) x • g x) x
⊢ ContMDiffAt I 𝓘(ℝ, G) (M' := G) ∞ (fun (x : M) ↦ (↑f : M → ℝ) x • g x) x
have this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
Tactic: have : x ∈ (chartAt H c).source :=
    f.tsupport_subset_chartAt_source <| tsupport_smul_subset_left _ _ hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u_5
M : Type u_6
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : IsEmpty H
⊢ IsEmpty M
have inl : ∀ (hM : IsEmpty M), IsEmpty M
Tactic: rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u_5
M : Type u_6
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : IsEmpty H
inl : ∀ (hM : IsEmpty M), IsEmpty M
⊢ IsEmpty M
have inr : ∀ (x : M), IsEmpty M
Tactic: rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
s : Set M
⊢ IsOpen[inst_1] s ↔ ∀ (x : M), IsOpen[inst] ((↑(chartAt H x) : M → H) '' ((toPartialEquiv (chartAt H x)).source ∩ s))
have rw : (∀ (i : M), IsOpen[inst_1] ((toPartialEquiv (chartAt H i)).source ∩ s)) ↔
  ∀ (x : M), IsOpen[inst] ((↑(chartAt H x) : M → H) '' ((toPartialEquiv (chartAt H x)).source ∩ s))
Tactic: rw [isOpen_iff_of_cover (fun i ↦ (chartAt H i).open_source) (iUnion_source_chartAt H M)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : SecondCountableTopology H
s : Set M
hs : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ
hsc : s.Countable
⊢ SecondCountableTopology M
have this : ∀ (x : M), SecondCountableTopology.{u_2} (↑(toPartialEquiv (chartAt H x)).source : Type u_2)
Tactic: haveI : ∀ x : M, SecondCountableTopology (chartAt H x).source :=
    fun x ↦ (chartAt (H := H) x).secondCountableTopology_source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : SecondCountableTopology H
s : Set M
hs : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ
hsc : s.Countable
this : ∀ (x : M), SecondCountableTopology.{u_2} (↑(toPartialEquiv (chartAt H x)).source : Type u_2)
⊢ SecondCountableTopology M
have haveI : ∀ (this : Encodable (↑s : Type u_2)), SecondCountableTopology M
Tactic: haveI := hsc.toEncodable
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : SecondCountableTopology H
s : Set M
hs : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ
hsc : s.Countable
this_1 : ∀ (x : M), SecondCountableTopology.{u_2} (↑(toPartialEquiv (chartAt H x)).source : Type u_2)
this : Encodable (↑s : Type u_2)
⊢ SecondCountableTopology M
have rw : ∀ (hs : Eq.{u_2 + 1} (α := Set M) (⋃ (x : (↑s : Type u_2)), (toPartialEquiv (chartAt H (↑x : M))).source) univ)
  (hsc : s.Countable)
  (this : ∀ (x : M), SecondCountableTopology.{u_2} (↑(toPartialEquiv (chartAt H x)).source : Type u_2))
  (this : Encodable (↑s : Type u_2)), SecondCountableTopology M
Tactic: rw [biUnion_eq_iUnion] at hs
Cleared hypotheses: hs, hsc, this_1, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : SecondCountableTopology H
inst_4 : SigmaCompactSpace M
⊢ SecondCountableTopology M
have obtain : ∀ (s : Set M) (hsc : s.Countable)
  (hsU : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ), SecondCountableTopology M
Tactic: obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
    countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyCompactSpace H
x : M
⊢ (𝓝 x).HasBasis
    (fun (s : Set H) ↦ s ∈ 𝓝 ((↑(chartAt H x) : M → H) x) ∧ IsCompact s ∧ s ⊆ (toPartialEquiv (chartAt H x)).target)
    fun (s : Set H) ↦ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s
have rw : (Filter.map (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) (𝓝 ((↑(chartAt H x) : M → H) x))).HasBasis
  (fun (s : Set H) ↦ s ∈ 𝓝 ((↑(chartAt H x) : M → H) x) ∧ IsCompact s ∧ s ⊆ (toPartialEquiv (chartAt H x)).target)
  fun (s : Set H) ↦ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s
Tactic: rw [← (chartAt H x).symm_map_nhds_eq (mem_chart_source H x)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyCompactSpace H
⊢ LocallyCompactSpace M
have this : ∀ (x : M),
  (𝓝 x).HasBasis
    (fun (s : Set H) ↦ s ∈ 𝓝 ((↑(chartAt H x) : M → H) x) ∧ IsCompact s ∧ s ⊆ (toPartialEquiv (chartAt H x)).target)
    fun (s : Set H) ↦ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s
Tactic: have : ∀ x : M, (𝓝 x).HasBasis
      (fun s ↦ s ∈ 𝓝 (chartAt H x x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target)
      fun s ↦ (chartAt H x).symm '' s := fun x ↦ by
    rw [← (chartAt H x).symm_map_nhds_eq (mem_chart_source H x)]
    exact ((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset
      (chart_target_mem_nhds H x)).map _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyCompactSpace H
this :
  ∀ (x : M),
    (𝓝 x).HasBasis
      (fun (s : Set H) ↦ s ∈ 𝓝 ((↑(chartAt H x) : M → H) x) ∧ IsCompact s ∧ s ⊆ (toPartialEquiv (chartAt H x)).target)
      fun (s : Set H) ↦ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s
⊢ LocallyCompactSpace M
have refine : ∀ (x : M) (i : Set H),
  i ∈ 𝓝 ((↑(chartAt H x) : M → H) x) ∧ IsCompact i ∧ i ⊆ (toPartialEquiv (chartAt H x)).target →
    IsCompact ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' i)
Tactic: refine .of_hasBasis this ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyConnectedSpace H
e : M → OpenPartialHomeomorph M H := chartAt H
⊢ LocallyConnectedSpace M
have refine_1 : ∀ (x : M),
  Filter.HasBasis.{u_2, u + 1} (ι := Set H) (𝓝 x)
    ((fun (x : M) (s : Set H) ↦ (IsOpen[inst] s ∧ (↑(e x) : M → H) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
    ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x)
Tactic: refine locallyConnectedSpace_of_connected_bases (fun x s ↦ (e x).symm '' s)
      (fun x s ↦ (IsOpen s ∧ e x x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocallyConnectedSpace H
e : M → OpenPartialHomeomorph M H := chartAt H
refine_1 :
  ∀ (x : M),
    Filter.HasBasis.{u_2, u + 1} (ι := Set H) (𝓝 x)
      ((fun (x : M) (s : Set H) ↦ (IsOpen[inst] s ∧ (↑(e x) : M → H) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x)
      ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x)
⊢ LocallyConnectedSpace M
have refine_2 : ∀ (x : M) (i : Set H),
  (fun (x : M) (s : Set H) ↦ (IsOpen[inst] s ∧ (↑(e x) : M → H) x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) x i →
    IsPreconnected.{u_2} (α := M) ((fun (x : M) (s : Set H) ↦ (↑(e x).symm : H → M) '' s) x i)
Tactic: refine locallyConnectedSpace_of_connected_bases (fun x s ↦ (e x).symm '' s)
      (fun x s ↦ (IsOpen s ∧ e x x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
⊢ LocPathConnectedSpace M
have refine : ∀ (x : M) (s : Set M) (hs : s ∈ 𝓝 x), ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
Tactic: refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have ht : t ∈ 𝓝 x
Tactic: have ht : t ∈ 𝓝 x := Filter.inter_mem hs (chart_source_mem_nhds _ _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have refine_1 : (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x
Tactic: refine ⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_1 : (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have refine_2 : IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
Tactic: refine ⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
refine_1 : (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x
refine_2 : IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
⊢ ∃ (i : Set M), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have refine_3 : id ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x)) ⊆ t
Tactic: refine ⟨e.symm '' pathComponentIn (e '' t) (e x), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 x
have refine_1 : (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e.symm : H → M) ((↑e : M → H) x))
Tactic: nth_rewrite 1 [← e.left_inv (mem_chart_source _ _)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ (↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e.symm : H → M) ((↑e : M → H) x))
have refine_1 : pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ∈ 𝓝 ((↑e : M → H) x)
Tactic: apply e.symm.image_mem_nhds (by simp [e])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ IsPathConnected ((↑e.symm : H → M) '' pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
have refine_2 : ContinuousOn (↑e.symm : H → M) (pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
Tactic: refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : LocPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ ContinuousOn (↑e.symm : H → M) (pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x))
have refine_2 : pathComponentIn ((↑e : M → H) '' t) ((↑e : M → H) x) ⊆ (↑e : M → H) '' e.source
Tactic: refine e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
⊢ T1Space M
have apply : ∀ (x y : M) (hxy : x ≠ y), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
Tactic: apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
have pos : ∀ (hy : y ∈ (toPartialEquiv (chartAt H x)).source), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
Tactic: by_cases hy : y ∈ (chartAt H x).source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
pos : ∀ (hy : y ∈ (toPartialEquiv (chartAt H x)).source), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
have neg : ∀ (hy : y ∉ (toPartialEquiv (chartAt H x)).source), ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
Tactic: by_cases hy : y ∈ (chartAt H x).source
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
have pos : IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ)
Tactic: refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
pos :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ)
⊢ ∃ (U : Set M), IsOpen[inst_1] U ∧ x ∈ U ∧ y ∉ U
have pos₁ : x ∈ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ
Tactic: refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (toPartialEquiv (chartAt H x)).source
⊢ x ∈ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) y}ᶜ
have pos : ¬(↑(chartAt H x) : M → H) x = (↑(chartAt H x) : M → H) y
Tactic: simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
        mem_singleton_iff, true_and]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
⊢ DiscreteTopology M
have apply : ∀ (x : M), IsOpen[inst_1] {x}
Tactic: apply discreteTopology_iff_isOpen_singleton.2 (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (hypothesis)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
⊢ IsOpen[inst_1] {x}
have this : IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
Tactic: have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
    isOpen_inter_preimage _ (isOpen_discrete _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
⊢ IsOpen[inst_1] {x}
have h : {x} = (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x}
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
⊢ {x} = (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x}
have h : (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x} ⊆ {x}
Tactic: refine Subset.antisymm (by simp) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : DiscreteTopology H
x : M
this :
  IsOpen[inst_1] ((toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x})
⊢ (toPartialEquiv (chartAt H x)).source ∩ (↑(chartAt H x) : M → H) ⁻¹' {(↑(chartAt H x) : M → H) x} ⊆ {x}
have h : ∀ y ∈ (toPartialEquiv (chartAt H x)).source, (↑(chartAt H x) : M → H) y = (↑(chartAt H x) : M → H) x → y = x
Tactic: simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u_5
H' : Type u_6
α : Type u_7
f : H → α
⊢ (range fun (p : ModelProd H H') ↦ (f p.1, p.2)) = SProd.sprod (β := Set H') (range f) univ
have rw : Eq (α := Set (α × H')) (range fun (p : ModelProd H H') ↦ (f p.1, p.2)) (range fun (p : H × H') ↦ (f p.1, p.2))
Tactic: rw [prod_range_univ_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
⊢ Eq (α := ChartedSpace (ModelProd H H') (H × H')) (prodChartedSpace H H H' H') (chartedSpaceSelf (H × H'))
have atlas : Eq (α := Set (OpenPartialHomeomorph (H × H') (ModelProd H H'))) ChartedSpace.atlas ChartedSpace.atlas
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
atlas : Eq (α := Set (OpenPartialHomeomorph (H × H') (ModelProd H H'))) ChartedSpace.atlas ChartedSpace.atlas
⊢ Eq (α := ChartedSpace (ModelProd H H') (H × H')) (prodChartedSpace H H H' H') (chartedSpaceSelf (H × H'))
have chartAt : Eq (α := H × H' → OpenPartialHomeomorph (H × H') (ModelProd H H')) ChartedSpace.chartAt ChartedSpace.chartAt
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
⊢ Eq (α := H × H' → OpenPartialHomeomorph (H × H') (ModelProd H H')) ChartedSpace.chartAt ChartedSpace.chartAt
have chartAt : ∀ (x : H × H'),
  Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (ChartedSpace.chartAt x) (ChartedSpace.chartAt x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
x : H × H'
⊢ Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (ChartedSpace.chartAt x) (ChartedSpace.chartAt x)
have chartAt : Eq (α := OpenPartialHomeomorph (H × H') (ModelProd H H')) (OpenPartialHomeomorph.refl (H × H'))
  (OpenPartialHomeomorph.refl (ModelProd H H'))
Tactic: simp only [prodChartedSpace_chartAt, chartAt_self_eq, refl_prod_refl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x w : M
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inl x)
have left : x ∈ PartialEquiv.source.{u_2, u} (β := H) (toPartialEquiv (ChartedSpace.chartAt x))
Tactic: use x, cm.mem_chart_source x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ChartedSpace (goal)
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst_3 : Nonempty H
x w : M
left : x ∈ PartialEquiv.source.{u_2, u} (β := H) (toPartialEquiv (ChartedSpace.chartAt x))
⊢ Membership.mem (γ := Set (M ⊕ M'))
    (PartialEquiv.source (β := H) (toPartialEquiv (lift_openEmbedding (ChartedSpace.chartAt x) ⋯))) (Sum.inl x)
have right : Eq (α := M ⊕ M') (Sum.inl x) (Sum.inl x)
Tactic: use x, cm.mem_chart_source x