awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.BumpFunction
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

Tactic:
contMDiff_of_tsupport fun x hx => ?_

Premises used: contMDiff_of_tsupport
-- Module: Mathlib.Geometry.Manifold.BumpFunction
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
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
⊢ ContMDiff I 𝓘(ℝ, G) (M' := G) ∞ fun (x : M) ↦ (↑f : M → ℝ) x • g x

Tactic:
refine contMDiff_of_tsupport fun x hx => ?_

Premises used: contMDiff_of_tsupport
-- Module: Mathlib.Geometry.Manifold.BumpFunction
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
⊢ x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
have : x ∈ (chartAt H c).source :=
    f.tsupport_subset_chartAt_source <| tsupport_smul_subset_left _ _ hx
-- Module: Mathlib.Geometry.Manifold.BumpFunction
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
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiffAt I 𝓘(ℝ, G) (M' := G) ∞ (fun (x : M) ↦ (↑f : M → ℝ) x • g x) x

Tactic:
f.contMDiffAt.smul ((hg _ this).contMDiffAt <| (chartAt _ _).open_source.mem_nhds this)

Premises used: chartAt, OpenPartialHomeomorph.open_source, ContMDiffAt.smul, ContMDiffWithinAt.contMDiffAt, SmoothBumpFunction.contMDiffAt, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.BumpFunction
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
this : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ ContMDiffAt I 𝓘(ℝ, G) (M' := G) ∞ (fun (x : M) ↦ (↑f : M → ℝ) x • g x) x

Tactic:
exact f.contMDiffAt.smul ((hg _ this).contMDiffAt <| (chartAt _ _).open_source.mem_nhds this)

Premises used: chartAt, OpenPartialHomeomorph.open_source, ContMDiffAt.smul, ContMDiffWithinAt.contMDiffAt, SmoothBumpFunction.contMDiffAt, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
M : Type u_6
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ x ∈ (toPartialEquiv (chartAt H x)).source

Tactic:
ChartedSpace.mem_chart_source x

Premises used: Set.Mem, ChartedSpace.mem_chart_source
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
M : Type u_6
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) (chartAt H x)

Tactic:
ChartedSpace.chart_mem_atlas x

Premises used: Set.Mem, ChartedSpace.chart_mem_atlas
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u_5
M : Type u_6
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ Nonempty H

Tactic:
⟨chartAt H x x⟩

Premises used: chartAt, OpenPartialHomeomorph.toFun', Nonempty.intro
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
inr : ∀ (x : M), IsEmpty M
⊢ IsEmpty M

Tactic:
rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
hM : IsEmpty M
⊢ IsEmpty M

Tactic:
hM
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
hM : IsEmpty M
⊢ IsEmpty M

Tactic:
exact hM
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
x : M
⊢ IsEmpty M

Tactic:
(IsEmpty.false (chartAt H x x)).elim

Premises used: chartAt, False.elim, OpenPartialHomeomorph.toFun', IsEmpty.false
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
x : M
⊢ IsEmpty M

Tactic:
exact (IsEmpty.false (chartAt H x x)).elim

Premises used: chartAt, False.elim, OpenPartialHomeomorph.toFun', IsEmpty.false
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ (↑(chartAt H x) : M → H) x ∈ (toPartialEquiv (chartAt H x)).target

Tactic:
(chartAt H x).map_source (mem_chart_source _ _)

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.map_source
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ (toPartialEquiv (chartAt H x)).source ∈ 𝓝 x

Tactic:
(chartAt H x).open_source.mem_nhds <| mem_chart_source H x

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.open_source, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ (toPartialEquiv (chartAt H x)).target ∈ 𝓝 ((↑(chartAt H x) : M → H) x)

Tactic:
(chartAt H x).open_target.mem_nhds <| mem_chart_target H x

Premises used: chartAt, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target, mem_chart_target
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
⊢ Eq.{u_2 + 1} (α := Set M) (⋃ (x : M), (toPartialEquiv (chartAt H x)).source) univ

Tactic:
eq_univ_iff_forall.mpr fun x ↦ mem_iUnion.mpr ⟨x, mem_chart_source H x⟩

Premises used: Iff.mpr, mem_chart_source, Set.eq_univ_iff_forall, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
s : Set M
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))
⊢ IsOpen[inst_1] 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)]

Premises used: isOpen_iff_of_cover, chartAt, OpenPartialHomeomorph.open_source, iUnion_source_chartAt
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
s : Set M
⊢ (∀ (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:
simp only [(chartAt H _).isOpen_image_iff_of_subset_source inter_subset_left]

Premises used: chartAt, OpenPartialHomeomorph.isOpen_image_iff_of_subset_source, Set.inter_subset_left
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ Eq (α := (↑(atlas H M) : Type (max u u_2))) (achart H x)
    (Subtype.mk (p := fun (x : OpenPartialHomeomorph M H) ↦
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) x) (chartAt H x) ⋯)

Tactic:
rfl

Premises used: achart, rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ Eq (α := OpenPartialHomeomorph M H) (↑(achart H x) : OpenPartialHomeomorph M H) (chartAt H x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
x : M
⊢ x ∈ (toPartialEquiv (↑(achart H x) : OpenPartialHomeomorph M H)).source

Tactic:
mem_chart_source H x

Premises used: mem_chart_source, Set.Mem
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ ∀ (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
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
haveI : ∀ (this : Encodable (↑s : Type u_2)), SecondCountableTopology M
⊢ SecondCountableTopology M

Tactic:
haveI := hsc.toEncodable
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
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
⊢ SecondCountableTopology M

Tactic:
rw [biUnion_eq_iUnion] at hs

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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 : Type u_2)), (toPartialEquiv (chartAt H (↑x : M))).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

Tactic:
secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

Premises used: chartAt, OpenPartialHomeomorph.open_source, TopologicalSpace.secondCountableTopology_of_countable_cover, Subtype.val
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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 : Type u_2)), (toPartialEquiv (chartAt H (↑x : M))).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

Tactic:
exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

Premises used: chartAt, OpenPartialHomeomorph.open_source, TopologicalSpace.secondCountableTopology_of_countable_cover, Subtype.val
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ ∃ (s : Set M), s.Countable ∧ Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ

Tactic:
countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x

Premises used: chart_source_mem_nhds, countable_cover_nhds_of_sigmaCompact
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
obtain :
  ∀ (s : Set M) (hsc : s.Countable)
    (hsU : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ), SecondCountableTopology M
⊢ 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

Premises used: chart_source_mem_nhds, Set.univ, countable_cover_nhds_of_sigmaCompact
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
s : Set M
hsc : s.Countable
hsU : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ
⊢ SecondCountableTopology M

Tactic:
ChartedSpace.secondCountable_of_countable_cover H hsU hsc

Premises used: ChartedSpace.secondCountable_of_countable_cover
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
s : Set M
hsc : s.Countable
hsU : Eq.{u_2 + 1} (α := Set M) (⋃ x ∈ s, (toPartialEquiv (chartAt H x)).source) univ
⊢ SecondCountableTopology M

Tactic:
exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc

Premises used: ChartedSpace.secondCountable_of_countable_cover
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
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
⊢ (𝓝 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)]

Premises used: OpenPartialHomeomorph.symm_map_nhds_eq, mem_chart_source, chartAt
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (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:
((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset
      (chart_target_mem_nhds H x)).map _

Premises used: chart_target_mem_nhds, chartAt, OpenPartialHomeomorph.toFun', Filter.HasBasis.map, compact_basis_nhds, Filter.HasBasis.hasBasis_self_subset
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
⊢ (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:
exact ((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset
      (chart_target_mem_nhds H x)).map _

Premises used: chart_target_mem_nhds, chartAt, OpenPartialHomeomorph.toFun', Filter.HasBasis.map, compact_basis_nhds, Filter.HasBasis.hasBasis_self_subset
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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

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 _
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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

Tactic:
.of_hasBasis this ?_

Premises used: LocallyCompactSpace.of_hasBasis
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
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)
⊢ LocallyCompactSpace M

Tactic:
refine .of_hasBasis this ?_
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
x : M
s : Set H
left : s ∈ 𝓝 ((↑(chartAt H x) : M → H) x)
h₂ : IsCompact s
h₃ : s ⊆ (toPartialEquiv (chartAt H x)).target
⊢ IsCompact ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s)

Tactic:
h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)

Premises used: chartAt, IsCompact.image_of_continuousOn, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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
x : M
s : Set H
left : s ∈ 𝓝 ((↑(chartAt H x) : M → H) x)
h₂ : IsCompact s
h₃ : s ⊆ (toPartialEquiv (chartAt H x)).target
⊢ IsCompact ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) '' s)

Tactic:
exact h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)

Premises used: chartAt, IsCompact.image_of_continuousOn, ContinuousOn.mono, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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

Tactic:
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) ?_ ?_

Premises used: IsConnected, PartialEquiv.target, Membership.mem, HasSubset.Subset, OpenPartialHomeomorph.toFun', And, Set.image, IsOpen, locallyConnectedSpace_of_connected_bases, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ChartedSpace
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)
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)
⊢ LocallyConnectedSpace M

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) ?_ ?_

Premises used: IsConnected, PartialEquiv.target, Membership.mem, HasSubset.Subset, OpenPartialHomeomorph.toFun', And, Set.image, IsOpen, locallyConnectedSpace_of_connected_bases, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm