α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ closure t
⊢ a * b ∈ s * t
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
⊢ s * closure t = s * t
refine' (mul_subset_iff.2 fun a ha b hb => _).antisymm (mul_subset_mul_left subset_closure)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
⊢ a * b ∈ s * t
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ closure t
⊢ a * b ∈ s * t
rw [mem_closure_iff] at hb
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
hbU : b ∈ s⁻¹ * {a * b}
⊢ a * b ∈ s * t
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
⊢ a * b ∈ s * t
have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, a * b, Set.inv_mem_inv.2 ha, rfl, inv_mul_cancel_left _ _⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
hbU : b ∈ s⁻¹ * {a * b}
c : α
hc : c ∈ s⁻¹
hcs : (fun x x_1 => x * x_1) c (a * b) ∈ t
⊢ a * b ∈ s * t
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
hbU : b ∈ s⁻¹ * {a * b}
⊢ a * b ∈ s * t
obtain ⟨_, ⟨c, d, hc, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
hs : IsOpen s
t : Set α
a : α
ha : a ∈ s
b : α
hb : ∀ (o : Set α), IsOpen o → b ∈ o → Set.Nonempty (o ∩ t)
hbU : b ∈ s⁻¹ * {a * b}
c : α
hc : c ∈ s⁻¹
hcs : (fun x x_1 => x * x_1) c (a * b) ∈ t
⊢ a * b ∈ s * t
exact ⟨c⁻¹, _, hc, hcs, inv_mul_cancel_left _ _⟩