awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
snd_φ : Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) = dl
rw :
  Eq (α := Filter (β × β))
    (comap (β := β × β) (⇑φ : (a : β × β) → β × β) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)))
    (comap (β := β × β) (⇑φ : (a : β × β) → β × β) (comap snd (𝓝 1)))
rw₁ :
  Eq (α := Filter (β × β))
    (comap (β := β) ((fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ (⇑φ : (a : β × β) → β × β)) (𝓝 1))
    (comap (β := β × β) (⇑φ : (a : β × β) → β × β) (comap snd (𝓝 1)))
rw₂ :
  Eq (α := Filter (β × β))
    (comap (β := β) ((fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ (⇑φ : (a : β × β) → β × β)) (𝓝 1))
    (comap (β := β) (Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β)) (𝓝 1))
rw₃ : comap dr (𝓝 1) = comap (β := β) (Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β)) (𝓝 1)
rw₄ : comap dr (𝓝 1) = comap dl (𝓝 1)
rw₅ : comap dr (𝓝 1) = 𝓤 β
rw₆ rw₇ : 𝓤 β = 𝓤 β
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))

Tactic:
rw [← (comap_injective φ.surjective).eq_iff, comap_comap, comap_comap, conj_φ, snd_φ,
      ← uniformity_eq_comap_inv_mul_nhds_one, ← uniformity_eq_comap_mul_inv_nhds_one]

Premises used: Function.Injective.eq_iff, uniformity_eq_comap_inv_mul_nhds_one, Filter.comap_injective, uniformity_eq_comap_mul_inv_nhds_one, Filter.comap_comap, Equiv.surjective
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
rw :
  LE.le.{u_2} (α := Filter (β × β)) (comap snd (𝓝 1)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1))
rw₁ rw₂ : LE.le.{u_2} (α := Filter (β × β)) (comap snd (𝓝 1)) (comap snd (𝓝 1))
⊢ Tendsto (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (comap snd (𝓝 1)) (𝓝 1)

Tactic:
rw [tendsto_iff_comap, comap_conj_nhds_one]

Premises used: comap_conj_nhds_one, Filter.tendsto_iff_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
rwa rwa₁ rwa₂ rwa₃ : Tendsto.{u_3, u_2} (β := β) (Function.comp (β := β × β) Prod.snd fun (i : ι) ↦ (g i, x i)) l (𝓝 1)
⊢ Tendsto.{u_3, u_2} (β := β × β) (fun (i : ι) ↦ (g i, x i)) l (comap Prod.snd (𝓝 1))

Tactic:
rwa [tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
⊢ Tendsto.{u_3, u_2} (β := β × β) (fun (i : ι) ↦ (g i, x i)) l (comap Prod.snd (𝓝 1))

Tactic:
have : Tendsto (fun i ↦ (g i, x i)) l (comap Prod.snd (𝓝 1)) := by
    rwa [tendsto_comap_iff]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
this : Tendsto.{u_3, u_2} (β := β × β) (fun (i : ι) ↦ (g i, x i)) l (comap Prod.snd (𝓝 1))
⊢ Tendsto.{u_3, u_2} (β := β) ((fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ fun (i : ι) ↦ (g i, x i)) l (𝓝 1)

Tactic:
tendsto_conj_nhds_one.comp this

Premises used: tendsto_conj_nhds_one, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
this : Tendsto.{u_3, u_2} (β := β × β) (fun (i : ι) ↦ (g i, x i)) l (comap Prod.snd (𝓝 1))
⊢ Tendsto (g * x * g⁻¹) l (𝓝 1)

Tactic:
convert! tendsto_conj_nhds_one.comp this

Premises used: tendsto_conj_nhds_one, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
rw :
  Tendsto (β := β)
    (Function.comp (β := (β × β) × β × β)
      ((fun (x : β × β) ↦ x.2 * x.1⁻¹) ∘ fun (x : (β × β) × β × β) ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2))
      fun (p : (β × β) × β × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ UniformContinuous (β := β) fun (p : β × β) ↦ p.1 / p.2

Tactic:
rw [UniformContinuous, uniformity_eq_comap_mul_inv_nhds_one β, tendsto_comap_iff,
        uniformity_prod_eq_prod, tendsto_map'_iff]

Premises used: UniformContinuous, Filter.tendsto_map'_iff, Filter.tendsto_comap_iff, uniformity_prod_eq_prod, uniformity_eq_comap_mul_inv_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto (β := β)
    (Function.comp (β := (β × β) × β × β)
      ((fun (x : β × β) ↦ x.2 * x.1⁻¹) ∘ fun (x : (β × β) × β × β) ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2))
      fun (p : (β × β) × β × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
simpa [Function.comp_def, div_eq_mul_inv, ← mul_assoc]

Premises used: mul_assoc, div_eq_mul_inv, Function.comp_def
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
suffices : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ UniformContinuous (β := β) fun (p : β × β) ↦ p.1 / p.2

Tactic:
suffices Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1) by
      rw [UniformContinuous, uniformity_eq_comap_mul_inv_nhds_one β, tendsto_comap_iff,
        uniformity_prod_eq_prod, tendsto_map'_iff]
      simpa [Function.comp_def, div_eq_mul_inv, ← mul_assoc]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
h : ∀ (x : (β × β) × β × β), φ x = (g * ψ * g⁻¹) x
⊢ φ = g * ψ * g⁻¹

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
x : (β × β) × β × β
⊢ φ x = (g * ψ * g⁻¹) x

Tactic:
simp [φ, ψ, g, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
⊢ φ = g * ψ * g⁻¹

Tactic:
have φ_ψ_conj : φ = g * ψ * g⁻¹ := by
      ext
      simp [φ, ψ, g, mul_assoc]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
rw : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (HMul.hMul (α := β) 1 1))
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
rw [← one_mul 1]

Premises used: OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (HMul.hMul (α := β) 1 1))

Tactic:
.mul ?_ ?_

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
refine_1 : Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
refine_2 : Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (HMul.hMul (α := β) 1 1))

Tactic:
refine .mul ?_ ?_
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
refine_1 :
  Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1)))
    (𝓝 1)
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one]

Premises used: uniformity_eq_comap_inv_mul_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1)))
    (𝓝 1)

Tactic:
tendsto_comap.comp tendsto_fst

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.1⁻¹ * x.2) (𝓝 1)))
    (𝓝 1)

Tactic:
exact tendsto_comap.comp tendsto_fst

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
refine_2 :
  Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1)))
    (𝓝 1)
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]

Premises used: uniformity_eq_comap_inv_mul_nhds_one_swapped
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1)))
    (𝓝 1)

Tactic:
tendsto_comap.comp tendsto_snd

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1)
    (SProd.sprod (α := Filter (β × β)) (β := Filter (β × β)) (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1))
      (comap (β := β) (fun (x : β × β) ↦ x.2⁻¹ * x.1) (𝓝 1)))
    (𝓝 1)

Tactic:
exact tendsto_comap.comp tendsto_snd

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
have ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1) := by
      rw [← one_mul 1]
      refine .mul ?_ ?_
      · rw [uniformity_eq_comap_inv_mul_nhds_one]
        exact tendsto_comap.comp tendsto_fst
      · rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
        exact tendsto_comap.comp tendsto_snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
φ_ψ_conj ▸ ψ_tendsto.conj_nhds_one g

Premises used: Eq.rec, Filter.Tendsto.conj_nhds_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun (x : (β × β) × β × β) ↦
    match (motive := (β × β) × β × β → β) x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
ψ_tendsto : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
exact φ_ψ_conj ▸ ψ_tendsto.conj_nhds_one g
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
γ : Type u_3
inst : Group γ
inst_1 : UniformSpace γ
⊢ IsUniformGroup γ ↔ IsLeftUniformGroup γ ∧ IsRightUniformGroup γ

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ .of_left_right⟩

Premises used: _private.0.isUniformGroup_iff_left_right.match_1, inferInstance, IsUniformGroup, And.intro, Iff.intro, IsUniformGroup.of_left_right
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 1, p x
⊢ ∀ᶠ (x : α) in 𝓝 1, ∀ (g : α), p (g * x * g⁻¹)

Tactic:
simpa using tendsto_conj_nhds_one.eventually hp

Premises used: tendsto_conj_nhds_one, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
rw :
  HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2 / x.1 ∈ U i}
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ {x : α × α | x.2 / x.1 ∈ U i}

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 α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2 / x.1 ∈ U i}

Tactic:
h.comap _

Premises used: Set.Mem, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
⊢ HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.2 / x.1 ∈ U i}

Tactic:
exact h.comap _

Premises used: Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : HasBasis (𝓝 1) p U
rw :
  HasBasis.{u_1, u_3} (α := α × α) (Filter.comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)) p fun (i : ι) ↦
    {x : α × α | x.1⁻¹ * x.2 ∈ U i}
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ {x : α × α | x.1⁻¹ * x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one]

Premises used: uniformity_eq_comap_inv_mul_nhds_one