awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
us : UniformSpace G
inst_1 : IsRightUniformGroup G
inst_2 : FirstCountableTopology G
N : Subgroup G
inst_3 : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace.{u_1} (G ⧸ N)
have hG₁ : CompleteSpace G
Tactic: rw [← this] at hG
Cleared hypotheses: hG, this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : FirstCountableTopology G
N : Subgroup G
inst_4 : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace.{u} (G ⧸ N)
have rw : ∀ (hG : CompleteSpace G), CompleteSpace.{u} (G ⧸ N)
Tactic: rw [← IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace] at hG ⊢
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
us : UniformSpace G
inst_1 : IsLeftUniformGroup G
inst_2 : FirstCountableTopology G
N : Subgroup G
inst_3 : N.Normal
hG : CompleteSpace G
⊢ IsTopologicalGroup.leftUniformSpace G = us
have h : 𝓤 G = 𝓤 G
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
us : UniformSpace G
inst_1 : IsLeftUniformGroup G
inst_2 : FirstCountableTopology G
N : Subgroup G
inst_3 : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G
have h : 𝓤 G = comap (β := G) (fun (x : G × G) ↦ x.1⁻¹ * x.2) (𝓝 1)
Tactic: rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
us : UniformSpace G
inst_1 : IsLeftUniformGroup G
inst_2 : FirstCountableTopology G
N : Subgroup G
inst_3 : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace.{u_1} (G ⧸ N)
have this : IsTopologicalGroup.leftUniformSpace G = us
Tactic: have : IsTopologicalGroup.leftUniformSpace G = us := by
    ext : 1
    rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
us : UniformSpace G
inst_1 : IsLeftUniformGroup G
inst_2 : FirstCountableTopology G
N : Subgroup G
inst_3 : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.leftUniformSpace G = us
⊢ CompleteSpace.{u_1} (G ⧸ N)
have hG₁ : CompleteSpace G
Tactic: rw [← this] at hG
Cleared hypotheses: hG, this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G
have rw : IsUniformGroup G
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G
have refine : ∀ (b : Bool), IsUniformGroup G
Tactic: refine isUniformGroup_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
b : Bool
⊢ IsUniformGroup G
have false : IsUniformGroup G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
b : Bool
false : IsUniformGroup G
⊢ IsUniformGroup G
have true : IsUniformGroup G
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G : Type u_1
H : Type u_2
hom : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : UniformSpace G
inst_3 : UniformSpace H
inst_4 : IsUniformGroup H
inst_5 : FunLike hom G H
inst_6 : MonoidHomClass hom G H
f : hom
hf : IsUniformInducing.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2
have simp_rw : UniformContinuous.{u_1, u_2} (β := H) fun (x : G × G) ↦
  HDiv.hDiv (α := H) (β := H) ((f : (a : G) → H) x.1 : H) ((f : (a : G) → H) x.2 : H)
Tactic: simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Constructions (goal)
Goal:
G_1 : Type u_1
H : Type u_2
hom : Type u_3
inst : Group G_1
inst_1 : Group H
ι : Type u_4
G : ι → Type u_5
inst_2 : (i : ι) → UniformSpace (G i)
inst_3 : (i : ι) → Group (G i)
inst_4 : ∀ (i : ι), IsUniformGroup.{u_5} (G i)
⊢ IsUniformGroup ((i : ι) → G i)
have rw : IsUniformGroup ((i : ι) → G i)
Tactic: rw [Pi.uniformSpace_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.1 * x.2⁻¹) (𝓝 1)
have rw : Eq.{u_3 + 1} (α := Filter (Gᵣ × Gᵣ)) (comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.swap.2 * x.swap.1⁻¹) (𝓝 1))
  (comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.1 * x.2⁻¹) (𝓝 1))
Tactic: rw [← comap_swap_uniformity, uniformity_eq_comap_mul_inv_nhds_one, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
Gₗ : Type u_2
inst : UniformSpace Gₗ
inst_1 : Group Gₗ
inst_2 : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (β := Gₗ) (fun (x : Gₗ × Gₗ) ↦ x.2⁻¹ * x.1) (𝓝 1)
have rw : Eq.{u_2 + 1} (α := Filter (Gₗ × Gₗ)) (comap (β := Gₗ) (fun (x : Gₗ × Gₗ) ↦ x.swap.1⁻¹ * x.swap.2) (𝓝 1))
  (comap (β := Gₗ) (fun (x : Gₗ × Gₗ) ↦ x.2⁻¹ * x.1) (𝓝 1))
Tactic: rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.2 / x.1) (𝓝 1)
have simp_rw : 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.2 * x.1⁻¹) (𝓝 1)
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.1 / x.2) (𝓝 1)
have rw : Eq.{u_3 + 1} (α := Filter (Gᵣ × Gᵣ)) (comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.swap.2 / x.swap.1) (𝓝 1))
  (comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.1 / x.2) (𝓝 1))
Tactic: rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
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 : β) ↦ (f x)⁻¹
have this : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1 / f x
Tactic: have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x
have this : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x / (g x)⁻¹
Tactic: have : UniformContinuous fun x => f x / (g x)⁻¹ := hf.div hg.inv
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (hypothesis)
Goal:
α : Type u_3
β : Type u_4
ι : Type u_5
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : ∀ i ∈ s, UniformContinuous (f i)), UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ s, f i x
h : ∀ i ∈ cons a s ha, UniformContinuous (f i)
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ cons a s ha, f i x
have h₁ : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
Tactic: simp_rw [Finset.mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
ι : Type u_5
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : ι → β → α
s : Finset ι
h : ∀ i ∈ s, UniformContinuous (f i)
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ s, f i x
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → UniformContinuous (f i)),
  UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ ∅, f i x
Tactic: induction s using Finset.cons_induction with
  | empty => simpa using uniformContinuous_const
  | cons a s ha ih =>
    simp_rw [Finset.mem_cons, forall_eq_or_imp] at h
    simpa [Finset.prod_cons] using h.1.mul (ih h.2)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
ι : Type u_5
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : ι → β → α
s : Finset ι
h : ∀ i ∈ s, UniformContinuous (f i)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → UniformContinuous (f i)),
    UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ ∅, f i x
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ s, f i x
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : ∀ (h : ∀ i ∈ s, UniformContinuous (f i)), UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ s, f i x)
  (h : ∀ i ∈ cons a s ha, UniformContinuous (f i)),
  UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ cons a s ha, f i x
Tactic: induction s using Finset.cons_induction with
  | empty => simpa using uniformContinuous_const
  | cons a s ha ih =>
    simp_rw [Finset.mem_cons, forall_eq_or_imp] at h
    simpa [Finset.prod_cons] using h.1.mul (ih h.2)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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 (𝓤 α)
have rw : Tendsto (f * g⁻¹) l (𝓤 α)
Tactic: rw [div_eq_mul_inv]
-- 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 α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0
have simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1
Tactic: simp_rw [pow_zero]
-- 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 α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ (n + 1)
have simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * f x ^ n
Tactic: simp_rw [pow_succ']
-- 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 α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ HPow.hPow (β := ℤ) (f x) (↑n : ℤ)
have simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ n
Tactic: simp_rw [zpow_natCast]
-- 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 α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x ^ Int.negSucc n
have simp_rw : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ (f x ^ (n + 1))⁻¹
Tactic: simp_rw [zpow_negSucc]
-- 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 α
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)
have refine : ∀ (𝓕 : Filter (α × α)), 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)
Tactic: refine eq_of_forall_le_iff fun 𝓕 ↦ ?_
-- 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 α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.2 * x.1⁻¹) (𝓝 1)
have rw : Tendsto id 𝓕 (𝓤 α) ↔
  Tendsto (HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)) 𝓕
    (𝓤 α)
Tactic: rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap,
      ← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_left, ← tendsto_id']
-- 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 α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)) 𝓕
      (𝓤 α)
have a : id = HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)
Tactic: congrm Tendsto ?_ _ _
-- 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 α
𝓕 : Filter (α × α)
⊢ id = HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)
have a : ∀ (x : α × α),
  (id x).1 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
        (fun (x : α × α) ↦ (x.1, x.1)) x).1
Tactic: ext
-- 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 α
𝓕 : 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
⊢ id = HMul.hMul (α := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹) fun (x : α × α) ↦ (x.1, x.1)
have a₁ : ∀ (x : α × α),
  (id x).2 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.2 * x.1⁻¹)
        (fun (x : α × α) ↦ (x.1, x.1)) x).2
Tactic: ext
-- 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 α
⊢ 𝓤 α = comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)
have refine : ∀ (𝓕 : Filter (α × α)), 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)
Tactic: refine eq_of_forall_le_iff fun 𝓕 ↦ ?_
-- 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 α
𝓕 : Filter (α × α)
⊢ 𝓕 ≤ 𝓤 α ↔ 𝓕 ≤ comap (β := α) (fun (x : α × α) ↦ x.1⁻¹ * x.2) (𝓝 1)
have rw : Tendsto id 𝓕 (𝓤 α) ↔
  Tendsto (HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)) 𝓕
    (𝓤 α)
Tactic: rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap,
      ← (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_right, ← tendsto_id']
-- 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 α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔
    Tendsto (HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2))
      𝓕 (𝓤 α)
have a : id = HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)
Tactic: congrm Tendsto ?_ _ _
-- 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 α
𝓕 : Filter (α × α)
⊢ id = HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)
have a : ∀ (x : α × α),
  (id x).1 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
        (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).1
Tactic: ext
-- 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 α
𝓕 : 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
⊢ id = HMul.hMul (α := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1)) (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2)
have a₁ : ∀ (x : α × α),
  (id x).2 =
    (HMul.hMul (α := α × α → α × α) (β := α × α → α × α) (fun (x : α × α) ↦ (x.1, x.1))
        (Prod.mk 1 ∘ fun (x : α × α) ↦ x.1⁻¹ * x.2) x).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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)
⊢ 𝓤 G = 𝓤 G
have rw : comap (β := G) (fun (x : G × G) ↦ x.2 / x.1) (𝓝 1) = 𝓤 G
Tactic: rw [(have := hu; uniformity_eq_comap_nhds_one), (have := hv; uniformity_eq_comap_nhds_one), h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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
⊢ 𝓤 G = 𝓤 G
have 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))
Tactic: rw [(have := hu; uniformity_eq_comap_nhds_one), (have := hv; uniformity_eq_comap_nhds_one), h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
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))
⊢ 𝓤 G = 𝓤 G
have 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))
Tactic: rw [(have := hu; uniformity_eq_comap_nhds_one), (have := hv; uniformity_eq_comap_nhds_one), h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Defs (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : IsCountablyGenerated.{u_1} (α := α) (𝓝 1)
⊢ (𝓤 α).IsCountablyGenerated
have rw : IsCountablyGenerated.{u_1} (α := α × α) (comap (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 1))
Tactic: rw [uniformity_eq_comap_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 ∘ (⇑φ : (a : β × β) → β × β) = dr
have h : ∀ (x : β × β), (conj ∘ (⇑φ : (a : β × β) → β × β)) x = dr 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 β
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)
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have conj_φ : conj ∘ (⇑φ : (a : β × β) → β × β) = dr
Tactic: have conj_φ : conj ∘ φ = dr := by
    ext; simp [conj, φ, dr]
-- 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
⊢ Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) = dl
have h : ∀ (x : β × β), Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) x = dl 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 β
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
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have snd_φ : Function.comp (β := β × β) snd (⇑φ : (a : β × β) → β × β) = dl
Tactic: have snd_φ : snd ∘ φ = dl := by
    ext; simp [φ, dl]
-- 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
⊢ Eq.{u_2 + 1} (α := Filter (β × β)) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)) (comap snd (𝓝 1))
have rw : Eq (α := Filter (β × β))
  (comap (β := β × β) (⇑φ : (a : β × β) → β × β) (comap (β := β) (fun (gx : β × β) ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 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]