[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
⊢ LocallyCompactSpace G
[PROOFSTEP]
refine' locally_compact_of_compact_nhds fun x => _
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x : G
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
obtain ⟨y, hy⟩ := K.interior_nonempty
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
let F := Homeomorph.mulLeft (x * y⁻¹)
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ∃ s, s ∈ 𝓝 x ∧ IsCompact s
[PROOFSTEP]
refine' ⟨F '' K, _, K.isCompact.image F.continuous⟩
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑F '' ↑K ∈ 𝓝 x
[PROOFSTEP]
suffices F.symm ⁻¹' K ∈ 𝓝 x by
  convert this using 1
  apply Equiv.image_eq_preimage
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K ∈ 𝓝 x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
⊢ ↑F '' ↑K = ↑(Homeomorph.symm F) ⁻¹' ↑K
[PROOFSTEP]
apply Equiv.image_eq_preimage
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) ⁻¹' ↑K ∈ 𝓝 x
[PROOFSTEP]
apply ContinuousAt.preimage_mem_nhds F.symm.continuous.continuousAt
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
[PROOFSTEP]
have : F.symm x = y := by
  simp only [Homeomorph.mulLeft_symm, mul_inv_rev, inv_inv, Homeomorph.coe_mulLeft, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
⊢ ↑(Homeomorph.symm F) x = y
[PROOFSTEP]
simp only [Homeomorph.mulLeft_symm, mul_inv_rev, inv_inv, Homeomorph.coe_mulLeft, 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
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 (↑(Homeomorph.symm F) x)
[PROOFSTEP]
rw [this]
[GOAL]
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K : PositiveCompacts G
x y : G
hy : y ∈ interior ↑K
F : G ≃ₜ G := Homeomorph.mulLeft (x * y⁻¹)
this : ↑(Homeomorph.symm F) x = y
⊢ ↑K ∈ 𝓝 y
[PROOFSTEP]
exact mem_interior_iff_mem_nhds.1 hy
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
let F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.1 • p.2
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
change Continuous F
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous F
[PROOFSTEP]
have H : Continuous (F ∘ fun p : G × G => (p.1, QuotientGroup.mk p.2)) :=
  by
  change Continuous fun p : G × G => QuotientGroup.mk (p.1 * p.2)
  refine' continuous_coinduced_rng.comp continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous (F ∘ fun p => (p.fst, ↑p.snd))
[PROOFSTEP]
change Continuous fun p : G × G => QuotientGroup.mk (p.1 * p.2)
[GOAL]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
⊢ Continuous fun p => ↑(p.fst * p.snd)
[PROOFSTEP]
refine' continuous_coinduced_rng.comp continuous_mul
[GOAL]
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
Γ : Subgroup G
inst✝ : LocallyCompactSpace G
F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.fst • p.snd
H : Continuous (F ∘ fun p => (p.fst, ↑p.snd))
⊢ Continuous F
[PROOFSTEP]
exact QuotientMap.continuous_lift_prod_right quotientMap_quotient_mk' H
