α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ 𝓤 α = 𝓤 α

α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.fst * a, x.snd * a)
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ comap (fun x => (x.fst * a, x.snd * a)) (𝓤 α) = 𝓤 α
nth_rewrite 1 [← uniformity_translate_mul a, comap_map]
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.fst * a, x.snd * a)
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ 𝓤 α = 𝓤 α

α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.fst * a, x.snd * a)
rfl
case mk.mk
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ (fun x => (x.fst * a, x.snd * a)) (p₁, p₂) = (fun x => (x.fst * a, x.snd * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.fst * a, x.snd * a)
rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩
no goals
case mk.mk
α : Type u_1
β : Type ?u.112462
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ (fun x => (x.fst * a, x.snd * a)) (p₁, p₂) = (fun x => (x.fst * a, x.snd * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)
simp only [Prod.mk.injEq, mul_left_inj, imp_self]