awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)))
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₁ : Eq (α := Filter (β × β)) (comap (β := β) ((fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ (⇑φ : (a : β × β) → β × β)) (𝓝 1))
  (comap (β := β × β) (⇑φ : (a : β × β) → β × β) (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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)))
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₂ : Eq (α := Filter (β × β)) (comap (β := β) ((fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ (⇑φ : (a : β × β) → β × β)) (𝓝 1))
  (comap (β := β) (Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β)) (𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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))
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₃ : comap dr (𝓝 1) = comap (β := β) (Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β)) (𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₄ : comap dr (𝓝 1) = comap dl (𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₅ : comap dr (𝓝 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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) = 𝓤 β
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw₆ : 𝓤 β = 𝓤 β
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
β : Type u_2
inst : UniformSpace β
inst_1 : Group β
inst_2 : IsLeftUniformGroup β
inst_3 : IsRightUniformGroup β
⊢ Tendsto (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (comap snd (𝓝 1)) (𝓝 1)
have rw : LE.le.{u_2} (α := Filter (β × β)) (comap snd (𝓝 1)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1))
Tactic: rw [tendsto_iff_comap, comap_conj_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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))
⊢ Tendsto (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (comap snd (𝓝 1)) (𝓝 1)
have rw₁ : LE.le.{u_2} (α := Filter (β × β)) (comap snd (𝓝 1)) (comap snd (𝓝 1))
Tactic: rw [tendsto_iff_comap, comap_conj_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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))
have rwa : Tendsto.{u_3, u_2} (β := β) (Function.comp (β := β × β) Prod.snd fun (i : ι) ↦ (g i, x i)) l (𝓝 1)
Tactic: rwa [tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
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 (g * x * g⁻¹) l (𝓝 1)
have this : 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
⊢ UniformContinuous (β := β) fun (p : β × β) ↦ p.1 / p.2
have 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)
Tactic: rw [UniformContinuous, uniformity_eq_comap_mul_inv_nhds_one β, tendsto_comap_iff,
        uniformity_prod_eq_prod, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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₁
⊢ UniformContinuous (β := β) fun (p : β × β) ↦ p.1 / p.2
have suffices : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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⁻¹
have h : ∀ (x : (β × β) × β × β), φ x = (g * ψ * g⁻¹) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
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₁
⊢ Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
have φ_ψ_conj : φ = g * ψ * g⁻¹
Tactic: have φ_ψ_conj : φ = g * ψ * g⁻¹ := by
      ext
      simp [φ, ψ, g, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
have rw : Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (HMul.hMul (α := β) 1 1))
Tactic: rw [← one_mul 1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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))
have refine_1 : Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.1.1⁻¹ x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Tactic: refine .mul ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
⊢ Tendsto ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (HMul.hMul (α := β) 1 1))
have refine_2 : Tendsto (β := β) (fun (x : (β × β) × β × β) ↦ HMul.hMul (α := β) x.2.2⁻¹ x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Tactic: refine .mul ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
have 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)
Tactic: rw [uniformity_eq_comap_inv_mul_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
have 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)
Tactic: rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
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)
have ψ_tendsto : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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 p fun (i : ι) ↦ {x : α × α | x.2 / x.1 ∈ U i}
have 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}
Tactic: rw [uniformity_eq_comap_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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 p fun (i : ι) ↦ {x : α × α | x.1⁻¹ * x.2 ∈ U i}
have 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}
Tactic: rw [uniformity_eq_comap_inv_mul_nhds_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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 p fun (i : ι) ↦ {x : α × α | x.1 / x.2 ∈ U i}
have 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}
Tactic: rw [uniformity_eq_comap_nhds_one_swapped]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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 p fun (i : ι) ↦ {x : α × α | x.2⁻¹ * x.1 ∈ U i}
have 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}
Tactic: rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
hom : Type u_3
inst_3 : UniformSpace β
inst_4 : Group β
inst_5 : IsUniformGroup β
inst_6 : FunLike hom α β
inst_7 : MonoidHomClass hom α β
f : hom
h : Tendsto.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β) (𝓝 1) (𝓝 1)
⊢ Eq (α := α × α → β) ((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2))
    fun (x : α × α) ↦ (f : (a : α) → β) (x.2 / x.1)
have h₁ : ∀ (x : α × α),
  Eq.{u_2 + 1} (α := β)
    (((fun (x : β × β) ↦ x.2 / x.1) ∘ fun (x : α × α) ↦ ((f : (a : α) → β) x.1, (f : (a : α) → β) x.2)) x : β)
    ((f : (a : α) → β) (x.2 / x.1) : β)
Tactic: ext