awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
⊢ UniformContinuous (β := α) fun (b : α) ↦ a * b

Tactic:
uniformContinuous_id.const_mul _

Premises used: UniformContinuous.const_mul, uniformContinuous_id
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
⊢ UniformContinuous (β := α) fun (b : α) ↦ b * a

Tactic:
uniformContinuous_id.mul_const _

Premises used: uniformContinuous_id, UniformContinuous.mul_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
a : α
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x / a

Tactic:
hf.div uniformContinuous_const

Premises used: UniformContinuous.div, uniformContinuous_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
⊢ UniformContinuous (β := α) fun (b : α) ↦ b / a

Tactic:
uniformContinuous_id.div_const _

Premises used: uniformContinuous_id, UniformContinuous.div_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
⊢ Tendsto (fun (p : (α × α) × α × α) ↦ p.1 * p.2) (𝓤 α ×ˢ 𝓤 α) (𝓤 α)

Tactic:
simpa [UniformContinuous, uniformity_prod_eq_prod] using uniformContinuous_mul (α := α)

Premises used: UniformContinuous, uniformContinuous_mul, uniformity_prod_eq_prod
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
⊢ Tendsto f⁻¹ l (𝓤 α)

Tactic:
have : Tendsto (· ⁻¹) (𝓤 α) (𝓤 α) := uniformContinuous_inv
  this.comp hf

Premises used: Filter.Tendsto.comp, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f : ι → α × α
l : Filter ι
⊢ Tendsto f⁻¹ l (𝓤 α) ↔ Tendsto f l (𝓤 α)

Tactic:
⟨fun H ↦ inv_inv f ▸ H.uniformity_inv, Filter.Tendsto.uniformity_inv⟩

Premises used: Eq.rec, Filter.Tendsto.uniformity_inv, inv_inv, Iff.intro
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
rw : Tendsto (f * g⁻¹) l (𝓤 α)
⊢ Tendsto (f / g) l (𝓤 α)

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
⊢ Tendsto (f * g⁻¹) l (𝓤 α)

Tactic:
hf.uniformity_mul hg.uniformity_inv

Premises used: Filter.Tendsto.uniformity_inv, Filter.Tendsto.uniformity_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
⊢ Tendsto (f * g⁻¹) l (𝓤 α)

Tactic:
exact hf.uniformity_mul hg.uniformity_inv

Premises used: Filter.Tendsto.uniformity_inv, Filter.Tendsto.uniformity_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto g l (𝓤 α)

Tactic:
simpa using hf.uniformity_inv.uniformity_mul hfg

Premises used: Filter.Tendsto.uniformity_inv, Filter.Tendsto.uniformity_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hg : Tendsto g l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto f l (𝓤 α)

Tactic:
simpa using hfg.uniformity_mul hg.uniformity_inv

Premises used: Filter.Tendsto.uniformity_inv, Filter.Tendsto.uniformity_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0

Tactic:
simp_rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1

Tactic:
uniformContinuous_const

Premises used: uniformContinuous_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1

Tactic:
exact uniformContinuous_const

Premises used: uniformContinuous_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * f x ^ n
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ (n + 1)

Tactic:
simp_rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * f x ^ n

Tactic:
hf.mul (hf.pow_const n)

Premises used: UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * f x ^ n

Tactic:
exact hf.mul (hf.pow_const n)

Premises used: UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
n : ℕ
⊢ UniformContinuous (β := α) fun (x : α) ↦ x ^ n

Tactic:
uniformContinuous_id.pow_const n

Premises used: UniformContinuous.pow_const, uniformContinuous_id
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ n
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ HPow.hPow (β := ℤ) (f x) (↑n : ℤ)

Tactic:
simp_rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ n

Tactic:
hf.pow_const _

Premises used: UniformContinuous.pow_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ n

Tactic:
exact hf.pow_const _

Premises used: UniformContinuous.pow_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ (f x ^ (n + 1))⁻¹
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ (f x ^ (n + 1))⁻¹

Tactic:
(hf.pow_const _).inv

Premises used: UniformContinuous.inv, UniformContinuous.pow_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ (f x ^ (n + 1))⁻¹

Tactic:
exact (hf.pow_const _).inv

Premises used: UniformContinuous.inv, UniformContinuous.pow_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
n : ℤ
⊢ UniformContinuous (β := α) fun (x : α) ↦ x ^ n

Tactic:
uniformContinuous_id.zpow_const n

Premises used: uniformContinuous_id, UniformContinuous.zpow_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
⊢ 𝓤 α = map (fun (x : α × α) ↦ (x.1 * a, x.2 * a)) (map (fun (x : α × α) ↦ (x.1 * a⁻¹, x.2 * a⁻¹)) (𝓤 α))

Tactic:
simp [Filter.map_map, Function.comp_def]

Premises used: Filter.map_map, Function.comp_def
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ IsUniformGroup.{u_1} αᵐᵒᵖ

Tactic:
⟨uniformContinuous_op.comp
      ((uniformContinuous_unop.comp uniformContinuous_snd).inv.mul <|
        uniformContinuous_unop.comp uniformContinuous_fst)⟩

Premises used: UniformContinuous.inv, uniformContinuous_snd, UniformContinuous.comp, MulOpposite.uniformContinuous_op, uniformContinuous_fst, UniformContinuous.mul, IsUniformGroup.mk, MulOpposite.uniformContinuous_unop
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
eq_of_forall_le_iff fun 𝓕 ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
refine : ∀ (𝓕 : Filter (α × α)), 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
refine eq_of_forall_le_iff fun 𝓕 ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
rw :
  Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)) 𝓕
      (𝓤 α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap,
      ← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_left, ← tendsto_id']

Premises used: tendsto_diag_uniformity, Filter.tendsto_id', Filter.tendsto_iff_comap, Prod.fst, Filter.comap_comap, nhds_eq_comap_uniformity, Filter.Tendsto.uniformity_mul_iff_left
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
a : id = HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)
⊢ Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)) 𝓕
      (𝓤 α)

Tactic:
congrm Tendsto ?_ _ _

Premises used: Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
a :
  ∀ (x : α × α),
    (id x).1 =
      (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
          (fun (x : α × α) ↦ (x.1, x.1)) x).1
a₁ :
  ∀ (x : α × α),
    (id x).2 =
      (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
          (fun (x : α × α) ↦ (x.1, x.1)) x).2
⊢ id = HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
x : α × α
⊢ (id x).1 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
        (fun (x : α × α) ↦ (x.1, x.1)) x).1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
x : α × α
⊢ (id x).2 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
        (fun (x : α × α) ↦ (x.1, x.1)) x).2

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)

Tactic:
eq_of_forall_le_iff fun 𝓕 ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
refine : ∀ (𝓕 : Filter (α × α)), 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)

Tactic:
refine eq_of_forall_le_iff fun 𝓕 ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
rw :
  Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2))
      𝓕 (𝓤 α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)

Tactic:
rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap,
      ← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_right, ← tendsto_id']

Premises used: tendsto_diag_uniformity, Filter.tendsto_id', Filter.tendsto_iff_comap, Prod.fst, Filter.comap_comap, Filter.Tendsto.uniformity_mul_iff_right, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
a : id = HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)
⊢ Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2))
      𝓕 (𝓤 α)

Tactic:
congrm Tendsto ?_ _ _

Premises used: Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
a :
  ∀ (x : α × α),
    (id x).1 =
      (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
          (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).1
a₁ :
  ∀ (x : α × α),
    (id x).2 =
      (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
          (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).2
⊢ id = HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
x : α × α
⊢ (id x).1 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
        (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
𝓕 : Filter (α × α)
x : α × α
⊢ (id x).2 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
        (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).2

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_3
inst : Group G
u v : UniformSpace G
hu : IsUniformGroup G
hv : IsUniformGroup G
h : Eq.{u_3 + 1} (α := Filter G) (𝓝 1) (𝓝 1)
rw : comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1) = 𝓤 G
rw₁ :
  Eq.{u_3 + 1} (α := Filter (G × G)) (comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1))
    (comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := Filter (G × G)) (comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1))
    (comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1))
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [(have := hu; uniformity_eq_comap_nhds_one), (have := hv; uniformity_eq_comap_nhds_one), h]

Premises used: uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_3
inst : Group G
u v : UniformSpace G
hu : IsUniformGroup G
hv : IsUniformGroup G
⊢ u = v ↔ Eq.{u_3 + 1} (α := Filter G) (𝓝 1) (𝓝 1)

Tactic:
⟨fun h => h ▸ rfl, hu.ext hv⟩

Premises used: IsUniformGroup.ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : IsCountablyGenerated.{u_1} (α := α) (𝓝 1)
rw : IsCountablyGenerated.{u_1} (α := α × α) (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1))
⊢ (𝓤 α).IsCountablyGenerated

Tactic:
rw [uniformity_eq_comap_nhds_one]

Premises used: uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : IsCountablyGenerated.{u_1} (α := α) (𝓝 1)
⊢ IsCountablyGenerated.{u_1} (α := α × α) (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1))

Tactic:
Filter.comap.isCountablyGenerated _ _

Premises used: Filter.comap.isCountablyGenerated
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : IsCountablyGenerated.{u_1} (α := α) (𝓝 1)
⊢ IsCountablyGenerated.{u_1} (α := α × α) (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1))

Tactic:
exact Filter.comap.isCountablyGenerated _ _

Premises used: Filter.comap.isCountablyGenerated
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
h : ∀ (x : β × β), (conj ∘ (⇑φ : (a : β × β) → β × β)) x = dr x
⊢ conj ∘ (⇑φ : (a : β × β) → β × β) = dr

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
x : β × β
⊢ (conj ∘ (⇑φ : (a : β × β) → β × β)) x = dr x

Tactic:
simp [conj, φ, dr]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
⊢ conj ∘ (⇑φ : (a : β × β) → β × β) = dr

Tactic:
have conj_φ : conj ∘ φ = dr := by
    ext; simp [conj, φ, dr]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ (⇑φ : (a : β × β) → β × β) = dr
h : ∀ (x : β × β), Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) x = dl x
⊢ Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) = dl

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ (⇑φ : (a : β × β) → β × β) = dr
x : β × β
⊢ Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) x = dl x

Tactic:
simp [φ, dl]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
dr : β × β → β := fun (xy : β × β) ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun (xy : β × β) ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun (b : β) ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ (⇑φ : (a : β × β) → β × β) = dr
⊢ Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) = dl

Tactic:
have snd_φ : snd ∘ φ = dl := by
    ext; simp [φ, dl]