α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.snd / x.fst) (𝓝 1)
rw [nhds_eq_comap_uniformity, Filter.comap_comap]
case refine'_1
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α) ≤ 𝓤 α

case refine'_2
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α) ≤ 𝓤 α
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
refine' le_antisymm (Filter.map_le_iff_le_comap.1 _) _
case refine'_1
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
case refine'_1
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α) ≤ 𝓤 α
intro s hs
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
case refine'_1
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_div hs with ⟨t, ht, hts⟩
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
⊢ t ⊆ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' s
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
refine' mem_map.2 (mem_of_superset ht _)
case refine'_1.intro.intro.mk
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
a b : α
⊢ (a, b) ∈ t → (a, b) ∈ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' s
case refine'_1.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
⊢ t ⊆ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' s
rintro ⟨a, b⟩
no goals
case refine'_1.intro.intro.mk
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a / c, b / c) ∈ s
a b : α
⊢ (a, b) ∈ t → (a, b) ∈ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' s
simpa [subset_def] using hts a b a
case refine'_2
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
case refine'_2
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α) ≤ 𝓤 α
intro s hs
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
case refine'_2
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_mul hs with ⟨t, ht, hts⟩
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
⊢ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' t ⊆ s
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.snd / x.fst) (𝓤 α)
refine' ⟨_, ht, _⟩
case refine'_2.intro.intro.mk
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
a b : α
⊢ (a, b) ∈ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' t → (a, b) ∈ s
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
⊢ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' t ⊆ s
rintro ⟨a, b⟩
no goals
case refine'_2.intro.intro.mk
α : Type u_1
β : Type ?u.159712
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set (α × α)
ht : t ∈ 𝓤 α
hts : ∀ (a b c : α), (a, b) ∈ t → (a * c, b * c) ∈ s
a b : α
⊢ (a, b) ∈ (Prod.mk 1 ∘ fun x => x.snd / x.fst) ⁻¹' t → (a, b) ∈ s
simpa [subset_def] using hts 1 (b / a) a