awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
n : ℕ
g : G
hg : g ∈ s
⊢ IsCompact (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))
have hc : IsCompact.{u_2} (X := X) ((fun (g : G) ↦ g • x) '' (K n ∩ g • V))
Tactic: suffices H : IsCompact ((fun (g : G) ↦ g • x) '' (K n ∩ g • V)) by
        simpa only [F, smul_singleton] using H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
n : ℕ
g : G
hg : g ∈ s
⊢ IsCompact.{u_2} (X := X) ((fun (g : G) ↦ g • x) '' (K n ∩ g • V))
have apply : IsCompact (K n ∩ g • V)
Tactic: apply IsCompact.image ?_ (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
⊢ Eq.{u_2 + 1} (α := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) univ
have apply : ∀ (y : X), Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) y
Tactic: apply eq_univ_iff_forall.2 (fun y ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
y : X
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) y
have obtain : ∀ (h : G), Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
Tactic: obtain ⟨h, rfl⟩ : ∃ h, h • x = y := exists_smul_eq G x y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
h : G
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
have obtain : ∀ (n : ℕ) (hn : h ∈ K n), Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
Tactic: obtain ⟨n, hn⟩ : ∃ n, h ∈ K n := exists_mem_compactCovering h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
h : G
n : ℕ
hn : h ∈ K n
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
have obtain : ∀ (g : G) (gs : g ∈ s) (hg : h ∈ g • V), Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
Tactic: obtain ⟨g, gs, hg⟩ : ∃ g ∈ s, h ∈ g • V := exists_set_mem_of_union_eq_top s _ hs _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
h : G
n : ℕ
hn : h ∈ K n
g : G
gs : g ∈ s
hg : h ∈ g • V
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) (h • x)
have simp : ∃ (a : ℕ), ∃ a_1 ∈ s, ∃ (x_1 : G), (x_1 ∈ K a ∧ x_1 ∈ a_1 • V) ∧ x_1 • x = h • x
Tactic: simp only [F, smul_singleton, mem_iUnion, mem_image, mem_inter_iff, Prod.exists,
        Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have obtain : ∀ (n : ℕ) (g : G) (hg : g ∈ s) (hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty),
  HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
Tactic: obtain ⟨⟨n, ⟨g, hg⟩⟩, hi⟩ : ∃ i, (interior (F i)).Nonempty := by
    have : Nonempty X := ⟨x⟩
    have : Encodable s := Countable.toEncodable s_count
    apply nonempty_interior_of_iUnion_of_closed
    · rintro ⟨n, ⟨g, hg⟩⟩
      apply IsCompact.isClosed
      suffices H : IsCompact ((fun (g : G) ↦ g • x) '' (K n ∩ g • V)) by
        simpa only [F, smul_singleton] using H
      apply IsCompact.image ?_ (by fun_prop)
      exact (isCompact_compactCovering G n).inter_right (V_closed.smul g)
    · apply eq_univ_iff_forall.2 (fun y ↦ ?_)
      obtain ⟨h, rfl⟩ : ∃ h, h • x = y := exists_smul_eq G x y
      obtain ⟨n, hn⟩ : ∃ n, h ∈ K n := exists_mem_compactCovering h
      obtain ⟨g, gs, hg⟩ : ∃ g ∈ s, h ∈ g • V := exists_set_mem_of_union_eq_top s _ hs _
      simp only [F, smul_singleton, mem_iUnion, mem_image, mem_inter_iff, Prod.exists,
        Subtype.exists, exists_prop]
      exact ⟨n, g, gs, h, ⟨hn, hg⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
⊢ (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
have apply : interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg)) ⊆ interior (HSMul.hSMul (β := Set X) (g • V) {x})
Tactic: apply hi.mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
⊢ interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg)) ⊆ interior (HSMul.hSMul (β := Set X) (g • V) {x})
have h : F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg) ⊆ HSMul.hSMul (β := Set X) (g • V) {x}
Tactic: apply interior_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
Tactic: have I : (interior ((g • V) • {x})).Nonempty := by
    apply hi.mono
    apply interior_mono
    exact smul_subset_smul_right inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
⊢ (interior (HSMul.hSMul (β := Set X) V {x})).Nonempty
have I₁ : (g • interior (HSMul.hSMul (β := Set X) V {x})).Nonempty
Tactic: rw [smul_assoc, interior_smul] at I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have obtain : ∀ (y : X) (hy : y ∈ interior (HSMul.hSMul (β := Set X) V {x})), HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
Tactic: obtain ⟨y, hy⟩ : (interior (V • ({x} : Set X))).Nonempty := by
    rw [smul_assoc, interior_smul] at I
    exact smul_set_nonempty.1 I
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
y : X
hy : y ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have obtain : ∀ (g' : G) (hg' : g' ∈ V) (hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})),
  HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
Tactic: obtain ⟨g', hg', rfl⟩ : ∃ g' ∈ V, g' • x = y := by simpa using interior_subset hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
have apply : x ∈ interior (HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x})
Tactic: apply mem_interior_iff_mem_nhds.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ x ∈ interior (HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x})
have rwa : x ∈ interior (g'⁻¹ • HSMul.hSMul (β := Set X) V {x})
Tactic: rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
rwa : x ∈ interior (g'⁻¹ • HSMul.hSMul (β := Set X) V {x})
⊢ x ∈ interior (HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x})
have rwa₁ : x ∈ g'⁻¹ • interior (HSMul.hSMul (β := Set X) V {x})
Tactic: rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have J : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
Tactic: have J : (g'⁻¹ • V) • {x} ∈ 𝓝 x := by
    apply mem_interior_iff_mem_nhds.1
    rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
J : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ⊆ HSMul.hSMul (β := Set X) U {x}
have a : g'⁻¹ • V ⊆ U
Tactic: apply smul_subset_smul_right
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
J : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
⊢ g'⁻¹ • V ⊆ U
have apply : V⁻¹ • V ⊆ U
Tactic: apply Subset.trans (smul_set_subset_smul (inv_mem_inv.2 hg')) ?_