-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformity_eq_comap_nhds_one : 𝓤 α = comap (fun x : α × α => x.2 / x.1) (𝓝 (1 : α))

Proof state:
case refine_2.intro.intro
α : Type u_1
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.2 / x.1) (𝓤 α)

Tactic:
refine ⟨_, ht, ?_⟩

Result:
case refine_2.intro.intro
α : Type u_1
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.2 / x.1) ⁻¹' t ⊆ s

Proof state:
case refine_2.intro.intro.mk
α : Type u_1
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.2 / x.1) ⁻¹' t → (a, b) ∈ s

Tactic:
simpa [subset_def] using hts 1 (b / a) a

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Tactic:
rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_mul hs with ⟨t, ht, hts⟩

Result:
case refine_2.intro.intro
α : Type u_1
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.2 / x.1) (𝓤 α)

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.2 / x.1) (𝓝 1)

Tactic:
rw [nhds_eq_comap_uniformity, Filter.comap_comap]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Proof state:
case refine_2.intro.intro
α : Type u_1
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.2 / x.1) ⁻¹' t ⊆ s

Tactic:
rintro ⟨a, b⟩

Result:
case refine_2.intro.intro.mk
α : Type u_1
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.2 / x.1) ⁻¹' t → (a, b) ∈ s

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Tactic:
refine le_antisymm (Filter.map_le_iff_le_comap.1 ?_) ?_

Result:
case refine_1
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ map (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α

case refine_2
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α

Proof state:
case refine_1
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Tactic:
rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_div hs with ⟨t, ht, hts⟩

Result:
case refine_1.intro.intro
α : Type u_1
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.2 / x.1) (𝓤 α)

Proof state:
case refine_1
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ map (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α

Tactic:
intro s hs

Result:
case refine_1
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Proof state:
case refine_1.intro.intro.mk
α : Type u_1
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.2 / x.1) ⁻¹' s

Tactic:
simpa [subset_def] using hts a b a

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α

Tactic:
intro s hs

Result:
case refine_2
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)

Proof state:
case refine_1.intro.intro
α : Type u_1
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.2 / x.1) ⁻¹' s

Tactic:
rintro ⟨a, b⟩

Result:
case refine_1.intro.intro.mk
α : Type u_1
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.2 / x.1) ⁻¹' s

Proof state:
case refine_1.intro.intro
α : Type u_1
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.2 / x.1) (𝓤 α)

Tactic:
refine mem_map.2 (mem_of_superset ht ?_)

Result:
case refine_1.intro.intro
α : Type u_1
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.2 / x.1) ⁻¹' s