[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a : G
⊢ Homeomorph.symm (Homeomorph.mulLeft a) = Homeomorph.mulLeft a⁻¹
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ ↑(Homeomorph.symm (Homeomorph.mulLeft a)) x✝ = ↑(Homeomorph.mulLeft a⁻¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a : G
⊢ Homeomorph.symm (Homeomorph.mulRight a) = Homeomorph.mulRight a⁻¹
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ ↑(Homeomorph.symm (Homeomorph.mulRight a)) x✝ = ↑(Homeomorph.mulRight a⁻¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ DiscreteTopology G
[PROOFSTEP]
rw [← singletons_open_iff_discrete]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
⊢ ∀ (a : G), IsOpen {a}
[PROOFSTEP]
intro g
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ IsOpen {g}
[PROOFSTEP]
suffices { g } = (fun x : G => g⁻¹ * x) ⁻¹' {1} by
  rw [this]
  exact (continuous_mul_left g⁻¹).isOpen_preimage _ h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen {g}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
this : {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
⊢ IsOpen ((fun x => g⁻¹ * x) ⁻¹' {1})
[PROOFSTEP]
exact (continuous_mul_left g⁻¹).isOpen_preimage _ h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsOpen {1}
g : G
⊢ {g} = (fun x => g⁻¹ * x) ⁻¹' {1}
[PROOFSTEP]
simp only [mul_one, Set.preimage_mul_left_singleton, eq_self_iff_true, inv_inv, Set.singleton_eq_singleton_iff]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Inv G
inst✝⁶ : ContinuousInv G
inst✝⁵ : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
[PROOFSTEP]
simp only [setOf_forall]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Inv G
inst✝⁶ : ContinuousInv G
inst✝⁵ : TopologicalSpace α
f : α → G
s : Set α
x : α
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed (⋂ (i : G₁), {x | x i⁻¹ = (x i)⁻¹})
[PROOFSTEP]
refine' isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹
[PROOFSTEP]
rw [← image_inv]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact (Inv.inv '' s)
[PROOFSTEP]
exact hs.image continuous_inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
rw [← sInf_range]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
exact continuousInv_sInf (Set.forall_range_iff.mpr h')
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
refine' continuousInv_iInf fun b => _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
b : Bool
⊢ ContinuousInv G
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
assumption
[GOAL]
case true
α : Type u
β : Type v
G : Type w
H : Type x
ι' : Sort u_1
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H✝ : Type x
G : Type u_1
H : Type u_2
inst✝⁴ : Inv G
inst✝³ : Inv H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv H
f : G → H
hf : Inducing f
hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹
⊢ Continuous (f ∘ fun a => a⁻¹)
[PROOFSTEP]
simpa only [(· ∘ ·), hf_inv] using hf.continuous.inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x : α
n : ℕ
⊢ Continuous fun a => a ^ Int.ofNat n
[PROOFSTEP]
simpa using continuous_pow n
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x : α
n : ℕ
⊢ Continuous fun a => a ^ Int.negSucc n
[PROOFSTEP]
simpa using (continuous_pow (n + 1)).inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))
[PROOFSTEP]
simp [tendsto_principal_principal]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))
[PROOFSTEP]
simp [tendsto_principal_principal]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[Ioi a⁻¹] a⁻¹) (𝓝[Iio a] a)
[PROOFSTEP]
simpa only [inv_inv] using @tendsto_inv_nhdsWithin_Ioi _ _ _ _ a⁻¹
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[Iio a⁻¹] a⁻¹) (𝓝[Ioi a] a)
[PROOFSTEP]
simpa only [inv_inv] using @tendsto_inv_nhdsWithin_Iio _ _ _ _ a⁻¹
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))
[PROOFSTEP]
simp [tendsto_principal_principal]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))
[PROOFSTEP]
simp [tendsto_principal_principal]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[Ici a⁻¹] a⁻¹) (𝓝[Iic a] a)
[PROOFSTEP]
simpa only [inv_inv] using @tendsto_inv_nhdsWithin_Ici _ _ _ _ a⁻¹
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f : α → G
s : Set α
x : α
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[Iic a⁻¹] a⁻¹) (𝓝[Ici a] a)
[PROOFSTEP]
simpa only [inv_inv] using @tendsto_inv_nhdsWithin_Iic _ _ _ _ a⁻¹
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x : α
S : Set G
hS : S ∈ 𝓝 1
⊢ S⁻¹ ∈ 𝓝 1
[PROOFSTEP]
rwa [← nhds_one_symm'] at hS
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Subgroup G
src✝ : Submonoid G := Submonoid.topologicalClosure s.toSubmonoid
g : G
hg :
  g ∈
    {
          toSubsemigroup :=
            { carrier := _root_.closure ↑s,
              mul_mem' := (_ : ∀ {a b : G}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
⊢ g⁻¹ ∈
    {
          toSubsemigroup :=
            { carrier := _root_.closure ↑s,
              mul_mem' := (_ : ∀ {a b : G}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
[PROOFSTEP]
simpa only [← Set.mem_inv, inv_closure, inv_coe_set] using hg
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs : Subgroup.topologicalClosure s = ⊤
⊢ Subgroup.topologicalClosure (Subgroup.map f s) = ⊤
[PROOFSTEP]
rw [SetLike.ext'_iff] at hs ⊢
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : ↑(Subgroup.topologicalClosure s) = ↑⊤
⊢ ↑(Subgroup.topologicalClosure (Subgroup.map f s)) = ↑⊤
[PROOFSTEP]
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)
[PROOFSTEP]
exact hf'.dense_image hf hs
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁷ : TopologicalSpace G✝
inst✝⁶ : Group G✝
inst✝⁵ : TopologicalGroup G✝
inst✝⁴ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
inst✝ : Normal N
n : G
hn : n ∈ topologicalClosure N
g : G
⊢ g * n * g⁻¹ ∈ topologicalClosure N
[PROOFSTEP]
apply map_mem_closure (TopologicalGroup.continuous_conj g) hn
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁷ : TopologicalSpace G✝
inst✝⁶ : Group G✝
inst✝⁵ : TopologicalGroup G✝
inst✝⁴ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
inst✝ : Normal N
n : G
hn : n ∈ topologicalClosure N
g : G
⊢ MapsTo (fun h => g * h * g⁻¹) ↑N ↑N
[PROOFSTEP]
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g * h ∈ connectedComponent 1
[PROOFSTEP]
rw [connectedComponent_eq hg]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g * h ∈ connectedComponent g
[PROOFSTEP]
have hmul : g ∈ connectedComponent (g * h) :=
  by
  apply Continuous.image_connectedComponent_subset (continuous_mul_left g)
  rw [← connectedComponent_eq hh]
  exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ connectedComponent (g * h)
[PROOFSTEP]
apply Continuous.image_connectedComponent_subset (continuous_mul_left g)
[GOAL]
case a
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun b => g * b) '' connectedComponent h
[PROOFSTEP]
rw [← connectedComponent_eq hh]
[GOAL]
case a
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun b => g * b) '' connectedComponent 1
[PROOFSTEP]
exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ (fun b => g * b) 1 = g
[PROOFSTEP]
simp only [mul_one]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent g
[PROOFSTEP]
simpa [← connectedComponent_eq hmul] using mem_connectedComponent
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1
[PROOFSTEP]
rw [← inv_one]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁶ : TopologicalSpace G✝
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalGroup G✝
inst✝³ : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1⁻¹
[PROOFSTEP]
exact Continuous.image_connectedComponent_subset continuous_inv _ ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / w ∈ s
[PROOFSTEP]
have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) := continuousAt_fst.mul continuousAt_snd.inv (by simpa)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 ((fun x => x.fst * x.snd⁻¹) (1, 1))
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Set G
hs : s ∈ 𝓝 1
this : (fun p => p.fst * p.snd⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v / w ∈ s
[PROOFSTEP]
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using this
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x✝ : α
x : G
⊢ 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x✝ : α
x : G
⊢ map ((fun x x_1 => x * x_1) x) (𝓝 1) = 𝓝 x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x✝ : α
x : G
⊢ map (fun y => y * x) (𝓝 1) = 𝓝 x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (𝓝 x) p fun i => {y | y / x ∈ s i}
[PROOFSTEP]
rw [← nhds_translation_mul_inv]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y / x ∈ s i}
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y * x⁻¹ ∈ s i}
[PROOFSTEP]
exact hb.comap _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
x : G
s : Set G
⊢ x ∈ closure s ↔ ∀ (U : Set G), U ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y / x ∈ U
[PROOFSTEP]
rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
x : G
s : Set G
⊢ (∀ (i : Set G), i ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y ∈ {y | y / x ∈ id i}) ↔ ∀ (U : Set G), U ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y / x ∈ U
[PROOFSTEP]
simp_rw [Set.mem_setOf, id]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝ : α
M : Type u_1
hom : Type u_2
inst✝³ : MulOneClass M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul M
inst✝ : MonoidHomClass hom G M
f : hom
hf : ContinuousAt (↑f) 1
x : G
⊢ ContinuousAt (↑f) x
[PROOFSTEP]
simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, (· ∘ ·), map_mul, map_one, mul_one] using
  hf.tendsto.const_mul (f x)
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (fun x => ↑(↑f x.fst) x.snd) (1, 1)
hl : ∀ (x : G), ContinuousAt (↑(↑f x)) 1
hr : ∀ (y : H), ContinuousAt (fun x => ↑(↑f x) y) 1
x✝ : G × H
x : G
y : H
⊢ ContinuousAt (fun x => ↑(↑f x.fst) x.snd) (x, y)
[PROOFSTEP]
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y, prod_map_map_eq,
  tendsto_map'_iff, (· ∘ ·), map_mul, MonoidHom.mul_apply] at *
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (↑(↑f x)) (𝓝 1) (𝓝 (↑(↑f x) 1))
hr : ∀ (y : H), Tendsto (fun x => ↑(↑f x) y) (𝓝 1) (𝓝 (↑(↑f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x => ↑(↑f x.fst) x.snd) (𝓝 1 ×ˢ 𝓝 1) (𝓝 (↑(↑f 1) 1))
⊢ Tendsto (fun x_1 => ↑(↑f x) y * ↑(↑f x_1.fst) y * (↑(↑f x) x_1.snd * ↑(↑f x_1.fst) x_1.snd)) (𝓝 1 ×ˢ 𝓝 1)
    (𝓝 (↑(↑f x) y))
[PROOFSTEP]
refine
  ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : TopologicalSpace α
f✝ : α → G
s : Set α
x✝¹ : α
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H →* M
hl : ∀ (x : G), Tendsto (↑(↑f x)) (𝓝 1) (𝓝 (↑(↑f x) 1))
hr : ∀ (y : H), Tendsto (fun x => ↑(↑f x) y) (𝓝 1) (𝓝 (↑(↑f 1) y))
x✝ : G × H
x : G
y : H
hf : Tendsto (fun x => ↑(↑f x.fst) x.snd) (𝓝 1 ×ˢ 𝓝 1) (𝓝 (↑(↑f 1) 1))
⊢ 𝓝 (↑(↑f x) y * ↑(↑f 1) y * (↑(↑f x) 1 * ↑(↑f 1) 1)) = 𝓝 (↑(↑f x) y)
[PROOFSTEP]
simp only [map_one, mul_one, MonoidHom.one_apply]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁴ : TopologicalSpace G✝
inst✝³ : Group G✝
inst✝² : TopologicalGroup G✝
inst✝¹ : TopologicalSpace α
f : α → G✝
s : Set α
x✝ : α
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : TopologicalGroup G
tg' : TopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ 𝓝 x = 𝓝 x
[PROOFSTEP]
rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ ContinuousInv G
[PROOFSTEP]
refine' ⟨continuous_iff_continuousAt.2 fun x₀ => _⟩
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ ContinuousAt (fun a => a⁻¹) x₀
[PROOFSTEP]
have : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map ((· * ·) x₀⁻¹) (𝓝 1)) :=
  (tendsto_map.comp <| hconj x₀).comp hinv
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
this : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map ((fun x x_1 => x * x_1) x₀⁻¹) (𝓝 1))
⊢ ContinuousAt (fun a => a⁻¹) x₀
[PROOFSTEP]
simpa only [ContinuousAt, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, (· ∘ ·), mul_assoc, mul_inv_rev,
  inv_mul_cancel_left] using this
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
[PROOFSTEP]
rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ← map_map, ← hleft, hright, map_map]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x => x * x₀⁻¹) ∘ fun x => x * x₀) (𝓝 1) = 𝓝 1
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ TopologicalGroup G
[PROOFSTEP]
refine' TopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => _
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
[PROOFSTEP]
replace hconj : ∀ x₀ : G, map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
[GOAL]
case hconj
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ ∀ (x₀ : G), map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
[PROOFSTEP]
exact fun x₀ => map_eq_of_inverse (fun x => x₀⁻¹ * x * x₀⁻¹⁻¹) (by ext; simp [mul_assoc]) (hconj _) (hconj _)
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀✝ x₀ : G
⊢ ((fun x => x₀ * x * x₀⁻¹) ∘ fun x => x₀⁻¹ * x * x₀⁻¹⁻¹) = id
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀✝ x₀ x✝ : G
⊢ ((fun x => x₀ * x * x₀⁻¹) ∘ fun x => x₀⁻¹ * x * x₀⁻¹⁻¹) x✝ = id x✝
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
[PROOFSTEP]
rw [← hconj x₀]
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x => x * x₀) (map (fun x => x₀ * x * x₀⁻¹) (𝓝 1))
[PROOFSTEP]
simpa [(· ∘ ·)] using hleft _
[GOAL]
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : TopologicalGroup G✝
inst✝² : TopologicalSpace α
f : α → G✝
s : Set α
x : α
G : Type u
inst✝¹ : CommGroup G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
[PROOFSTEP]
simpa using tendsto_id
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
⊢ IsOpenMap mk
[PROOFSTEP]
intro s s_op
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk '' s)
[PROOFSTEP]
change IsOpen (((↑) : G → G ⧸ N) ⁻¹' ((↑) '' s))
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))
[PROOFSTEP]
rw [QuotientGroup.preimage_image_mk N s]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s)
[PROOFSTEP]
exact isOpen_iUnion fun n => (continuous_mul_right _).isOpen_preimage s s_op
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
have cont : Continuous (((↑) : G → G ⧸ N) ∘ fun p : G × G ↦ p.fst * p.snd) := continuous_quot_mk.comp continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
have quot : QuotientMap fun p : G × G ↦ ((p.1 : G ⧸ N), (p.2 : G ⧸ N)) :=
  by
  apply IsOpenMap.to_quotientMap
  · exact (QuotientGroup.isOpenMap_coe N).prod (QuotientGroup.isOpenMap_coe N)
  · exact continuous_quot_mk.prod_map continuous_quot_mk
  · exact (surjective_quot_mk _).Prod_map (surjective_quot_mk _)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
⊢ QuotientMap fun p => (↑p.fst, ↑p.snd)
[PROOFSTEP]
apply IsOpenMap.to_quotientMap
[GOAL]
case open_map
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
⊢ IsOpenMap fun p => (↑p.fst, ↑p.snd)
[PROOFSTEP]
exact (QuotientGroup.isOpenMap_coe N).prod (QuotientGroup.isOpenMap_coe N)
[GOAL]
case cont
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
⊢ Continuous fun p => (↑p.fst, ↑p.snd)
[PROOFSTEP]
exact continuous_quot_mk.prod_map continuous_quot_mk
[GOAL]
case surj
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
⊢ Surjective fun p => (↑p.fst, ↑p.snd)
[PROOFSTEP]
exact (surjective_quot_mk _).Prod_map (surjective_quot_mk _)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
cont : Continuous (QuotientGroup.mk ∘ fun p => p.fst * p.snd)
quot : QuotientMap fun p => (↑p.fst, ↑p.snd)
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
exact quot.continuous_iff.2 cont
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
⊢ Continuous fun a => a⁻¹
[PROOFSTEP]
have quot := IsOpenMap.to_quotientMap (QuotientGroup.isOpenMap_coe N) continuous_quot_mk (surjective_quot_mk _)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
quot : QuotientMap QuotientGroup.mk
⊢ Continuous fun a => a⁻¹
[PROOFSTEP]
rw [quot.continuous_iff]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n inst✝ : Subgroup.Normal N
quot : QuotientMap QuotientGroup.mk
⊢ Continuous ((fun a => a⁻¹) ∘ QuotientGroup.mk)
[PROOFSTEP]
exact continuous_quot_mk.comp continuous_inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
rcases(𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
[GOAL]
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
have := ((hu.prod_nhds hu).tendsto_iff hu).mp (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
⊢ Tendsto ?m.498154 (𝓝 (1, 1)) (𝓝 1)
[PROOFSTEP]
simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G)
[GOAL]
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), True → ∃ ia, (True ∧ True) ∧ ∀ (x : G × G), x ∈ u ia.fst ×ˢ u ia.snd → x.fst * x.snd ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
simp only [and_self_iff, mem_prod, and_imp, Prod.forall, exists_true_left, Prod.exists, forall_true_left] at this
[GOAL]
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n :=
  by
  intro n
  rcases this n with ⟨j, k, -, h⟩
  refine' atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => _⟩
  rintro - ⟨a, b, ha, hb, rfl⟩
  exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
⊢ ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
[PROOFSTEP]
intro n
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n : ℕ
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
[PROOFSTEP]
rcases this n with ⟨j, k, -, h⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
⊢ ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
[PROOFSTEP]
refine' atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => _⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
⊢ u m * u m ⊆ u n
[PROOFSTEP]
rintro - ⟨a, b, ha, hb, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n✝ : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
n j k : ℕ
h : ∀ (a b : G), a ∈ u j → b ∈ u k → a * b ∈ u n
m : ℕ
hm : m ∈ Ici (max j k)
a b : G
ha : a ∈ u m
hb : b ∈ u m
⊢ (fun x x_1 => x * x_1) a b ∈ u n
[PROOFSTEP]
exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
[GOAL]
case intro.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
[GOAL]
case intro.mk.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : HasBasis (𝓝 1) (fun x => True) u
u_anti : Antitone u
this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib
event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n
φ : ℕ → ℕ
hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)
φ_anti_basis : HasAntitoneBasis (𝓝 1) (u ∘ φ)
⊢ ∃ u, HasAntitoneBasis (𝓝 1) u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
[PROOFSTEP]
exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
⊢ Continuous fun p => p.fst / p.snd
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
⊢ Continuous fun p => p.fst * p.snd⁻¹
[PROOFSTEP]
exact continuous_fst.mul continuous_snd.inv
[GOAL]
α✝ : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto (fun n => u n / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)
[PROOFSTEP]
simpa using h.mul A
[GOAL]
α✝ : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 => x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun n => u n / x) l (𝓝 1)
[PROOFSTEP]
simpa using h.div' A
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
x : G
⊢ comap (fun x_1 => x_1 / x) (𝓝 1) = 𝓝 x
[PROOFSTEP]
simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
ht : IsOpen t
⊢ IsOpen (s • t)
[PROOFSTEP]
rw [← iUnion_smul_set]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
ht : IsOpen t
⊢ IsOpen (⋃ (a : α) (_ : a ∈ s), a • t)
[PROOFSTEP]
exact isOpen_biUnion fun a _ => ht.smul _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
a : α
x : β
ht : t ∈ 𝓝 x
⊢ a • t ∈ 𝓝 (a • x)
[PROOFSTEP]
rcases mem_nhds_iff.1 ht with ⟨u, ut, u_open, hu⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
a : α
x : β
ht : t ∈ 𝓝 x
u : Set β
ut : u ⊆ t
u_open : IsOpen u
hu : x ∈ u
⊢ a • t ∈ 𝓝 (a • x)
[PROOFSTEP]
exact mem_nhds_iff.2 ⟨a • u, smul_set_mono ut, u_open.smul a, smul_mem_smul_set hu⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (s • t)
[PROOFSTEP]
have : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t := by
  intro x ⟨g, y, hgs, hyt, hgyx⟩
  refine ⟨g, hgs, ?_⟩
  convert hyt
  rwa [inv_smul_eq_iff, eq_comm]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
⊢ ∀ (x : β), x ∈ s • t → ∃ g, g ∈ s ∧ g⁻¹ • x ∈ t
[PROOFSTEP]
intro x ⟨g, y, hgs, hyt, hgyx⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
x : β
g : α
y : β
hgs : g ∈ s
hyt : y ∈ t
hgyx : (fun x x_1 => x • x_1) g y = x
⊢ ∃ g, g ∈ s ∧ g⁻¹ • x ∈ t
[PROOFSTEP]
refine ⟨g, hgs, ?_⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
x : β
g : α
y : β
hgs : g ∈ s
hyt : y ∈ t
hgyx : (fun x x_1 => x • x_1) g y = x
⊢ g⁻¹ • x ∈ t
[PROOFSTEP]
convert hyt
[GOAL]
case h.e'_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
x : β
g : α
y : β
hgs : g ∈ s
hyt : y ∈ t
hgyx : (fun x x_1 => x • x_1) g y = x
⊢ g⁻¹ • x = y
[PROOFSTEP]
rwa [inv_smul_eq_iff, eq_comm]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
this : ∀ (x : β), x ∈ s • t → ∃ g, g ∈ s ∧ g⁻¹ • x ∈ t
⊢ IsClosed (s • t)
[PROOFSTEP]
choose! f hf using this
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
⊢ IsClosed (s • t)
[PROOFSTEP]
refine isClosed_of_closure_subset (fun x hx ↦ ?_)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
x : β
hx : x ∈ closure (s • t)
⊢ x ∈ s • t
[PROOFSTEP]
rcases mem_closure_iff_ultrafilter.mp hx with ⟨u, hust, hux⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
x : β
hx : x ∈ closure (s • t)
u : Ultrafilter β
hust : s • t ∈ u
hux : ↑u ≤ 𝓝 x
⊢ x ∈ s • t
[PROOFSTEP]
have : Ultrafilter.map f u ≤ 𝓟 s :=
  calc
    Ultrafilter.map f u ≤ map f (𝓟 (s • t)) := map_mono (le_principal_iff.mpr hust)
    _ = 𝓟 (f '' (s • t)) := map_principal
    _ ≤ 𝓟 s := principal_mono.mpr (image_subset_iff.mpr (fun x hx ↦ (hf x hx).1))
[GOAL]
case intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
x : β
hx : x ∈ closure (s • t)
u : Ultrafilter β
hust : s • t ∈ u
hux : ↑u ≤ 𝓝 x
this : ↑(Ultrafilter.map f u) ≤ 𝓟 s
⊢ x ∈ s • t
[PROOFSTEP]
rcases hs.ultrafilter_le_nhds (Ultrafilter.map f u) this with ⟨g, hg, hug⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
x : β
hx : x ∈ closure (s • t)
u : Ultrafilter β
hust : s • t ∈ u
hux : ↑u ≤ 𝓝 x
this : ↑(Ultrafilter.map f u) ≤ 𝓟 s
g : α
hg : g ∈ s
hug : ↑(Ultrafilter.map f u) ≤ 𝓝 g
⊢ x ∈ s • t
[PROOFSTEP]
suffices g⁻¹ • x ∈ t from ⟨g, g⁻¹ • x, hg, this, smul_inv_smul _ _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
f : β → α
hf : ∀ (x : β), x ∈ s • t → f x ∈ s ∧ (f x)⁻¹ • x ∈ t
x : β
hx : x ∈ closure (s • t)
u : Ultrafilter β
hust : s • t ∈ u
hux : ↑u ≤ 𝓝 x
this : ↑(Ultrafilter.map f u) ≤ 𝓟 s
g : α
hg : g ∈ s
hug : ↑(Ultrafilter.map f u) ≤ 𝓝 g
⊢ g⁻¹ • x ∈ t
[PROOFSTEP]
exact ht.mem_of_tendsto ((Tendsto.inv hug).smul hux) (Eventually.mono hust (fun y hy ↦ (hf y hy).2))
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
s : Set α
t : Set β
inst✝ : CompactSpace α
⊢ IsClosedMap Quotient.mk'
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
s : Set α
t✝ : Set β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (Quotient.mk' '' t)
[PROOFSTEP]
rw [← quotientMap_quotient_mk'.isClosed_preimage, MulAction.quotient_preimage_image_eq_union_mul]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
s : Set α
t✝ : Set β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ IsClosed (⋃ (g : α), (fun x x_1 => x • x_1) g '' t)
[PROOFSTEP]
convert ht.smul_left_of_isCompact (isCompact_univ (α := α))
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
s : Set α
t✝ : Set β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ (g : α), (fun x x_1 => x • x_1) g '' t = univ • t
[PROOFSTEP]
rw [← biUnion_univ, ← iUnion_smul_left_image]
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
s : Set α
t✝ : Set β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed t
⊢ ⋃ (x : α) (_ : x ∈ univ), (fun x x_1 => x • x_1) x '' t = ⋃ (a : α) (_ : a ∈ univ), a • t
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)
[PROOFSTEP]
have := smul_mem_nhds a h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s t : Set α
a b : α
h : s ∈ 𝓝 b
this : a • s ∈ 𝓝 (a • b)
⊢ {a} * s ∈ 𝓝 (a * b)
[PROOFSTEP]
rwa [← singleton_smul] at this
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s t : Set α
a : α
h : s ∈ 𝓝 1
⊢ {a} * s ∈ 𝓝 a
[PROOFSTEP]
simpa only [mul_one] using singleton_mul_mem_nhds a h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (s * t)
[PROOFSTEP]
rw [← iUnion_op_smul_set]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), op a • s)
[PROOFSTEP]
exact isOpen_biUnion fun a _ => hs.smul _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)
[PROOFSTEP]
simp only [← iUnion_op_smul_set, mem_singleton_iff, iUnion_iUnion_eq_left]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a b : α
h : s ∈ 𝓝 b
⊢ op a • s ∈ 𝓝 (b * a)
[PROOFSTEP]
exact smul_mem_nhds _ h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a
[PROOFSTEP]
simpa only [one_mul] using mul_singleton_mem_nhds a h
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
ht : IsOpen t
⊢ IsOpen (s / t)
[PROOFSTEP]
rw [← iUnion_div_left_image]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
ht : IsOpen t
⊢ IsOpen (⋃ (a : α) (_ : a ∈ s), (fun x x_1 => x / x_1) a '' t)
[PROOFSTEP]
exact isOpen_biUnion fun a _ => isOpenMap_div_left a t ht
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
hs : IsOpen s
⊢ IsOpen (s / t)
[PROOFSTEP]
rw [← iUnion_div_right_image]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), (fun x => x / a) '' s)
[PROOFSTEP]
exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs
[GOAL]
α : 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
[PROOFSTEP]
refine' (mul_subset_iff.2 fun a ha b hb => _).antisymm (mul_subset_mul_left subset_closure)
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_closure_iff] at hb
[GOAL]
α : 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
[PROOFSTEP]
have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, a * b, Set.inv_mem_inv.2 ha, rfl, inv_mul_cancel_left _ _⟩
[GOAL]
α : 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
[PROOFSTEP]
obtain ⟨_, ⟨c, d, hc, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
[GOAL]
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
[PROOFSTEP]
exact ⟨c⁻¹, _, hc, hcs, inv_mul_cancel_left _ _⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s✝ t : Set α
ht : IsOpen t
s : Set α
⊢ closure s * t = s * t
[PROOFSTEP]
rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv, inv_inv]
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s✝ t : Set α
ht : IsOpen t
s : Set α
⊢ closure s / t = s / t
[PROOFSTEP]
simp_rw [div_eq_mul_inv, ht.inv.closure_mul]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (t * s)
[PROOFSTEP]
rw [← image_op_smul]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (op '' s • t)
[PROOFSTEP]
exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
H : Subgroup α
hH : IsCompact ↑H
⊢ IsClosedMap mk
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
H : Subgroup α
hH : IsCompact ↑H
t : Set α
ht : IsClosed t
⊢ IsClosed (mk '' t)
[PROOFSTEP]
rw [← quotientMap_quotient_mk'.isClosed_preimage]
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
H : Subgroup α
hH : IsCompact ↑H
t : Set α
ht : IsClosed t
⊢ IsClosed (Quotient.mk' ⁻¹' (mk '' t))
[PROOFSTEP]
convert ht.mul_right_of_isCompact hH
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
H : Subgroup α
hH : IsCompact ↑H
t : Set α
ht : IsClosed t
⊢ Quotient.mk' ⁻¹' (mk '' t) = t * ↑H
[PROOFSTEP]
refine (QuotientGroup.preimage_image_mk_eq_iUnion_image _ _).trans ?_
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
H : Subgroup α
hH : IsCompact ↑H
t : Set α
ht : IsClosed t
⊢ ⋃ (x : { x // x ∈ H }), (fun x_1 => x_1 * ↑x) '' t = t * ↑H
[PROOFSTEP]
rw [iUnion_subtype, ← iUnion_mul_right_image]
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t✝ : Set α
H : Subgroup α
hH : IsCompact ↑H
t : Set α
ht : IsClosed t
⊢ ⋃ (x : α) (hx : x ∈ H), (fun x_1 => x_1 * ↑{ val := x, property := hx }) '' t =
    ⋃ (a : α) (_ : a ∈ ↑H), (fun x => x * a) '' t
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed {1}
x : G
⊢ IsClosed {x}
[PROOFSTEP]
convert isClosedMap_mul_right x _ h
[GOAL]
case h.e'_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed {1}
x : G
⊢ {x} = (fun x_1 => x_1 * x) '' {1}
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
⊢ RegularSpace G
[PROOFSTEP]
refine' RegularSpace.ofExistsMemNhdsIsClosedSubset fun a s hs => _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
[PROOFSTEP]
have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) := continuous_mul.tendsto' _ _ (mul_one a)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p => p.fst * p.snd) (𝓝 (a, 1)) (𝓝 a)
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
[PROOFSTEP]
rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p => p.fst * p.snd) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : U ×ˢ V ⊆ (fun p => p.fst * p.snd) ⁻¹' s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
[PROOFSTEP]
rw [← image_subset_iff, image_prod] at hUV
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p => p.fst * p.snd) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : image2 HMul.hMul U V ⊆ s
⊢ ∃ t, t ∈ 𝓝 a ∧ IsClosed t ∧ t ⊆ s
[PROOFSTEP]
refine' ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p => p.fst * p.snd) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : image2 HMul.hMul U V ⊆ s
⊢ closure U ⊆ s
[PROOFSTEP]
calc
  closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
  _ = U * interior V := (isOpen_interior.closure_mul U)
  _ ⊆ U * V := (mul_subset_mul_left interior_subset)
  _ ⊆ s := hUV
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T0Space G
⊢ T2Space G
[PROOFSTEP]
haveI := TopologicalGroup.t3Space G
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T0Space G
this : T3Space G
⊢ T2Space G
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
S✝ : Subgroup G
inst✝² : Normal S✝
inst✝¹ : IsClosed ↑S✝
S : Subgroup G
inst✝ : Normal S
hS : IsClosed ↑S
⊢ T3Space (G ⧸ S)
[PROOFSTEP]
rw [← QuotientGroup.ker_mk' S] at hS
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
S✝ : Subgroup G
inst✝² : Normal S✝
inst✝¹ : IsClosed ↑S✝
S : Subgroup G
inst✝ : Normal S
hS : IsClosed ↑(MonoidHom.ker (QuotientGroup.mk' S))
⊢ T3Space (G ⧸ S)
[PROOFSTEP]
haveI := TopologicalGroup.t1Space (G ⧸ S) (quotientMap_quotient_mk'.isClosed_preimage.mp hS)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
S✝ : Subgroup G
inst✝² : Normal S✝
inst✝¹ : IsClosed ↑S✝
S : Subgroup G
inst✝ : Normal S
hS : IsClosed ↑(MonoidHom.ker (QuotientGroup.mk' S))
this : T1Space (G ⧸ S)
⊢ T3Space (G ⧸ S)
[PROOFSTEP]
exact TopologicalGroup.t3Space _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
intro K L hK hL
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)ᶜ)ᶜ
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
rw [preimage_compl, compl_compl] at H
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
convert H
[GOAL]
case h.e'_2
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
[PROOFSTEP]
simp only [image_smul, mem_setOf_eq, coeSubtype, mem_preimage, mem_image, Prod.exists]
[GOAL]
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x
[PROOFSTEP]
exact Set.smul_inter_ne_empty_iff'
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
intro K L hK hL
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prod_map continuous_id
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
have H : Set.Finite _ := hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' (((fun p => p.fst * p.snd) ∘ fun p => (p.fst⁻¹, p.snd)) '' K ×ˢ L)ᶜ)ᶜ
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
simp only [preimage_compl, compl_compl, coeSubtype, comp_apply] at H
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L))
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
[PROOFSTEP]
apply Finite.of_preimage _ (oppositeEquiv S).surjective
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L))
⊢ Set.Finite (↑(oppositeEquiv S) ⁻¹' {γ | (fun x => γ • x) '' K ∩ L ≠ ∅})
[PROOFSTEP]
convert H using 1
[GOAL]
case h.e'_2
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L))
⊢ ↑(oppositeEquiv S) ⁻¹' {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L))
x : { x // x ∈ S }
⊢ x ∈ ↑(oppositeEquiv S) ⁻¹' {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔
    x ∈ Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L)
[PROOFSTEP]
simp only [image_smul, mem_setOf_eq, coeSubtype, mem_preimage, mem_image, Prod.exists]
[GOAL]
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous fun p => (p.fst⁻¹, p.snd)
H : Set.Finite (Subtype.val ⁻¹' ((fun a => a.fst⁻¹ * a.snd) '' K ×ˢ L))
x : { x // x ∈ S }
⊢ ↑(oppositeEquiv S) x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = ↑x
[PROOFSTEP]
exact Set.op_smul_inter_ne_empty_iff
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ K * V ⊆ U
[PROOFSTEP]
refine hK.induction_on ?_ ?_ ?_ ?_
[GOAL]
case refine_1
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∅ * V ⊆ U
[PROOFSTEP]
exact ⟨univ, by simp⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ U
[PROOFSTEP]
simp
[GOAL]
case refine_2
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U
[PROOFSTEP]
rintro s t hst ⟨V, hV, hV'⟩
[GOAL]
case refine_2.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t : Set G
hst : s ⊆ t
V : Set G
hV : V ∈ 𝓝 1
hV' : t * V ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U
[PROOFSTEP]
exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
[GOAL]
case refine_3
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V, V ∈ 𝓝 1 ∧ s * V ⊆ U) → (∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U) → ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U
[PROOFSTEP]
rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
[GOAL]
case refine_3.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ (s ∪ t) * V ⊆ U
[PROOFSTEP]
use V ∩ W, inter_mem V_in W_in
[GOAL]
case right
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U
[PROOFSTEP]
rw [union_mul]
[GOAL]
case right
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
[PROOFSTEP]
exact
  union_subset ((mul_subset_mul_left (V.inter_subset_left W)).trans hV')
    ((mul_subset_mul_left (V.inter_subset_right W)).trans hW')
[GOAL]
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∀ (x : G), x ∈ K → ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
intro x hx
[GOAL]
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 1)
[PROOFSTEP]
simpa using hU.mem_nhds (hKU hx)
[GOAL]
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : U ∈ map (fun p => p.fst * p.snd) (𝓝 (x, 1))
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
[GOAL]
case refine_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : ∃ t₁, t₁ ∈ 𝓝 x ∧ ∃ t₂, t₂ ∈ 𝓝 1 ∧ t₁ ×ˢ t₂ ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
rcases this with ⟨t, ht, s, hs, h⟩
[GOAL]
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t ×ˢ s ⊆ (fun p => p.fst * p.snd) ⁻¹' U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
rw [← image_subset_iff, image_mul_prod] at h
[GOAL]
case refine_4.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t, t ∈ 𝓝[K] x ∧ ∃ V, V ∈ 𝓝 1 ∧ t * V ⊆ U
[PROOFSTEP]
exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ U
[PROOFSTEP]
rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
    (image_subset op hKU) with
  ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : op '' K * V ⊆ op '' U⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ ∃ V, V ∈ 𝓝 1 ∧ V * K ⊆ U
[PROOFSTEP]
refine' ⟨op ⁻¹' V, continuous_op.continuousAt hV, _⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
V : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op '' K * V ⊆ op '' U
⊢ op ⁻¹' V * K ⊆ U
[PROOFSTEP]
rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff, preimage_image_eq _ op_injective] at hV'
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ ∃ t, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
[PROOFSTEP]
obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((· * ·) x ⁻¹' V) :=
  by
  refine' hK.elim_finite_subcover (fun x => interior <| (· * ·) x ⁻¹' V) (fun x => isOpen_interior) _
  cases' hV with g₀ hg₀
  refine' fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, _⟩
  refine' preimage_interior_subset_interior_preimage (continuous_const.mul continuous_id) _
  rwa [mem_preimage, id_def, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ ∃ t, K ⊆ ⋃ (x : G) (_ : x ∈ t), interior ((fun x x_1 => x * x_1) x ⁻¹' V)
[PROOFSTEP]
refine' hK.elim_finite_subcover (fun x => interior <| (· * ·) x ⁻¹' V) (fun x => isOpen_interior) _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
⊢ K ⊆ ⋃ (i : G), (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) i
[PROOFSTEP]
cases' hV with g₀ hg₀
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ (i : G), (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) i
[PROOFSTEP]
refine' fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, _⟩
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => interior ((fun x x_1 => x * x_1) x ⁻¹' V)) (g₀ * g⁻¹)
[PROOFSTEP]
refine' preimage_interior_subset_interior_preimage (continuous_const.mul continuous_id) _
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => g₀ * g⁻¹ * id x) ⁻¹' interior V
[PROOFSTEP]
rwa [mem_preimage, id_def, inv_mul_cancel_right]
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
K V : Set G
hK : IsCompact K
hV : Set.Nonempty (interior V)
t : Finset G
ht : K ⊆ ⋃ (x : G) (_ : x ∈ t), interior ((fun x x_1 => x * x_1) x ⁻¹' V)
⊢ ∃ t, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V
[PROOFSTEP]
exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
⊢ SigmaCompactSpace G
[PROOFSTEP]
obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
[GOAL]
case intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ SigmaCompactSpace G
[PROOFSTEP]
refine' ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, _, _⟩⟩
[GOAL]
case intro.intro.refine'_1
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ∀ (n : ℕ), IsCompact ((fun n => (fun x => x * denseSeq G n) ⁻¹' L) n)
[PROOFSTEP]
intro n
[GOAL]
case intro.intro.refine'_1
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
n : ℕ
⊢ IsCompact ((fun n => (fun x => x * denseSeq G n) ⁻¹' L) n)
[PROOFSTEP]
exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc
[GOAL]
case intro.intro.refine'_2
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ (n : ℕ), (fun n => (fun x => x * denseSeq G n) ⁻¹' L) n = univ
[PROOFSTEP]
refine' iUnion_eq_univ_iff.2 fun x => _
[GOAL]
case intro.intro.refine'_2
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
⊢ ∃ i, x ∈ (fun n => (fun x => x * denseSeq G n) ⁻¹' L) i
[PROOFSTEP]
obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty :=
  by
  rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
  exact (denseRange_denseSeq G).inter_nhds_nonempty ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
⊢ Set.Nonempty (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L)
[PROOFSTEP]
rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
x : G
hL1 : L ∈ 𝓝 (↑(Homeomorph.mulLeft x) (↑(Homeomorph.symm (Homeomorph.mulLeft x)) 1))
⊢ Set.Nonempty (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L)
[PROOFSTEP]
exact (denseRange_denseSeq G).inter_nhds_nonempty ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
[GOAL]
case intro.intro.refine'_2.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : LocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
n : ℕ
hn : denseSeq G n ∈ (fun y => x * y) ⁻¹' L
⊢ ∃ i, x ∈ (fun n => (fun x => x * denseSeq G n) ⁻¹' L) i
[PROOFSTEP]
exact ⟨n, hn⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ ∃ g, Disjoint K (g • L)
[PROOFSTEP]
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, Disjoint K (g • L)
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
  contrapose! A
  exact eq_univ_iff_forall.2 A
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, ¬g ∈ K * L⁻¹
[PROOFSTEP]
contrapose! A
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ
[PROOFSTEP]
exact eq_univ_iff_forall.2 A
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ ∃ g, Disjoint K (g • L)
[PROOFSTEP]
refine' ⟨g, _⟩
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ Disjoint K (g • L)
[PROOFSTEP]
refine disjoint_left.2 fun a ha h'a => hg ?_
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
⊢ g ∈ K * L⁻¹
[PROOFSTEP]
rcases h'a with ⟨b, bL, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ g ∈ K * L⁻¹
[PROOFSTEP]
refine' ⟨g * b, b⁻¹, ha, by simpa only [Set.mem_inv, inv_inv] using bL, _⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ b⁻¹ ∈ L⁻¹
[PROOFSTEP]
simpa only [Set.mem_inv, inv_inv] using bL
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ (fun x x_1 => x * x_1) (g * b) b⁻¹ = g
[PROOFSTEP]
simp only [smul_eq_mul, mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
[PROOFSTEP]
obtain ⟨L, Lint, LU, Lcomp⟩ : ∃ (L : Set G), L ∈ 𝓝 (1 : G) ∧ L ⊆ U ∧ IsCompact L := local_compact_nhds hU
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
[PROOFSTEP]
obtain ⟨V, Vnhds, hV⟩ : ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v * w ∈ L :=
  by
  have : (fun p : G × G => p.1 * p.2) ⁻¹' L ∈ 𝓝 ((1, 1) : G × G) :=
    by
    refine' continuousAt_fst.mul continuousAt_snd _
    simpa only [mul_one] using Lint
  simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using this
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
[PROOFSTEP]
have : (fun p : G × G => p.1 * p.2) ⁻¹' L ∈ 𝓝 ((1, 1) : G × G) :=
  by
  refine' continuousAt_fst.mul continuousAt_snd _
  simpa only [mul_one] using Lint
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
⊢ (fun p => p.fst * p.snd) ⁻¹' L ∈ 𝓝 (1, 1)
[PROOFSTEP]
refine' continuousAt_fst.mul continuousAt_snd _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
⊢ L ∈ 𝓝 ((fun x => x.fst * x.snd) (1, 1))
[PROOFSTEP]
simpa only [mul_one] using Lint
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
this : (fun p => p.fst * p.snd) ⁻¹' L ∈ 𝓝 (1, 1)
⊢ ∃ V, V ∈ 𝓝 1 ∧ ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
[PROOFSTEP]
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using this
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
[PROOFSTEP]
have VL : closure V ⊆ L :=
  calc
    closure V = {(1 : G)} * closure V := by simp only [singleton_mul, one_mul, image_id']
    _ ⊆ interior V * closure V :=
      (mul_subset_mul_right (by simpa only [singleton_subset_iff] using mem_interior_iff_mem_nhds.2 Vnhds))
    _ = interior V * V := (isOpen_interior.mul_closure _)
    _ ⊆ V * V := (mul_subset_mul_right interior_subset)
    _ ⊆ L := by
      rintro x ⟨y, z, yv, zv, rfl⟩
      exact hV _ yv _ zv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
⊢ closure V = {1} * closure V
[PROOFSTEP]
simp only [singleton_mul, one_mul, image_id']
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
⊢ {1} ⊆ interior V
[PROOFSTEP]
simpa only [singleton_subset_iff] using mem_interior_iff_mem_nhds.2 Vnhds
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
⊢ V * V ⊆ L
[PROOFSTEP]
rintro x ⟨y, z, yv, zv, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
y z : G
yv : y ∈ V
zv : z ∈ V
⊢ (fun x x_1 => x * x_1) y z ∈ L
[PROOFSTEP]
exact hV _ yv _ zv
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : LocallyCompactSpace G
U : Set G
hU : U ∈ 𝓝 1
L : Set G
Lint : L ∈ 𝓝 1
LU : L ⊆ U
Lcomp : IsCompact L
V : Set G
Vnhds : V ∈ 𝓝 1
hV : ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w ∈ L
VL : closure V ⊆ L
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
[PROOFSTEP]
exact
  ⟨closure V, isCompact_of_isClosed_subset Lcomp isClosed_closure VL, isClosed_closure, VL.trans LU,
    interior_mono subset_closure (mem_interior_iff_mem_nhds.2 Vnhds)⟩
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ 𝓝 (x * y) = map (fun x_1 => x * x_1) (map (fun x => x * y) (𝓝 1 * 𝓝 1))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map (fun x_1 => x * x_1) (map (fun x => x * y) (𝓝 1 * 𝓝 1)) = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1)
[PROOFSTEP]
rw [← map₂_mul, map_map₂, map_map₂]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1)
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y
[PROOFSTEP]
rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left, map₂_map_right]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
g : G
⊢ Continuous fun x => g • x
[PROOFSTEP]
convert ((@continuous_const _ _ _ _ g).mul continuous_id).quotient_map' _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
x : G ⧸ Γ
⊢ Continuous fun g => g • x
[PROOFSTEP]
induction x using QuotientGroup.induction_on
[GOAL]
case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
Γ : Subgroup G
z✝ : G
⊢ Continuous fun g => g • ↑z✝
[PROOFSTEP]
exact continuous_quotient_mk'.comp (continuous_mul_right _)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
rw [← sInf_range]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
exact topologicalGroup_sInf (Set.forall_range_iff.mpr h')
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : TopologicalGroup G
h₂ : TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : TopologicalGroup G
h₂ : TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
refine' topologicalGroup_iInf fun b => _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : TopologicalGroup G
h₂ : TopologicalGroup G
b : Bool
⊢ TopologicalGroup G
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : TopologicalGroup G
h₂ : TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
assumption
[GOAL]
case true
α : Type u
β : Type v
G : Type w
H : Type x
ι : Sort u_1
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : TopologicalGroup G
h₂ : TopologicalGroup G
⊢ TopologicalGroup G
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
letI := g.toTopologicalSpace
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
haveI := g.toTopologicalGroup
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : TopologicalGroup α
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
exact continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
⊢ Continuous Inv.inv
[PROOFSTEP]
letI := g.toTopologicalSpace
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous Inv.inv
[PROOFSTEP]
haveI := g.toTopologicalGroup
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : TopologicalGroup α
⊢ Continuous Inv.inv
[PROOFSTEP]
exact continuous_inv
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
g : GroupTopology α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
toTopologicalSpace✝¹ : TopologicalSpace α
toTopologicalGroup✝¹ : TopologicalGroup α
toTopologicalSpace✝ : TopologicalSpace α
toTopologicalGroup✝ : TopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toTopologicalGroup := toTopologicalGroup✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toTopologicalGroup := toTopologicalGroup✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
_t : TopologicalSpace α := ⊥
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
haveI := discreteTopology_bot α
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
_t : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
src✝¹ : InfSet (GroupTopology α) := inferInstanceAs (InfSet (GroupTopology α))
src✝ : PartialOrder (GroupTopology α) := inferInstanceAs (PartialOrder (GroupTopology α))
⊢ ∀ (s : Set (GroupTopology α)) (a : GroupTopology α), (∀ (b : GroupTopology α), b ∈ s → a ≤ b) → a ≤ sInf s
[PROOFSTEP]
intro S a hab
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
src✝¹ : InfSet (GroupTopology α) := inferInstanceAs (InfSet (GroupTopology α))
src✝ : PartialOrder (GroupTopology α) := inferInstanceAs (PartialOrder (GroupTopology α))
S : Set (GroupTopology α)
a : GroupTopology α
hab : ∀ (b : GroupTopology α), b ∈ S → a ≤ b
⊢ a ≤ sInf S
[PROOFSTEP]
apply (inferInstanceAs (CompleteLattice (TopologicalSpace α))).le_sInf
[GOAL]
case a
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
src✝¹ : InfSet (GroupTopology α) := inferInstanceAs (InfSet (GroupTopology α))
src✝ : PartialOrder (GroupTopology α) := inferInstanceAs (PartialOrder (GroupTopology α))
S : Set (GroupTopology α)
a : GroupTopology α
hab : ∀ (b : GroupTopology α), b ∈ S → a ≤ b
⊢ ∀ (b : TopologicalSpace α), b ∈ toTopologicalSpace '' S → a.toTopologicalSpace ≤ b
[PROOFSTEP]
rintro _ ⟨b, hbS, rfl⟩
[GOAL]
case a.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝ : Group α
src✝¹ : InfSet (GroupTopology α) := inferInstanceAs (InfSet (GroupTopology α))
src✝ : PartialOrder (GroupTopology α) := inferInstanceAs (PartialOrder (GroupTopology α))
S : Set (GroupTopology α)
a : GroupTopology α
hab : ∀ (b : GroupTopology α), b ∈ S → a ≤ b
b : GroupTopology α
hbS : b ∈ S
⊢ a.toTopologicalSpace ≤ b.toTopologicalSpace
[PROOFSTEP]
exact hab b hbS
[GOAL]
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ Continuous f
[PROOFSTEP]
rw [continuous_sInf_rng]
[GOAL]
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ (t_1 : TopologicalSpace β),
    t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace} → Continuous f
[PROOFSTEP]
rintro _ ⟨t', ht', rfl⟩
[GOAL]
case intro.intro
α✝ : Type u
β✝ : Type v
G : Type w
H : Type x
inst✝¹ : Group α✝
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous f
[PROOFSTEP]
exact continuous_iff_coinduced_le.2 ht'