awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : DiscreteTopology.{u_1} ↥H
hd : IsDiscrete (↑H : Set G)
V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
VH : V ∩ (↑H : Set G) = {1}
this : (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ (↑H : Set G)
h' : G
h'_in : h' ∈ (↑H : Set G)
⊢ h ≠ h' → (fun (x y : G) ↦ (x, y) ∉ (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'
have contrapose : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (h, h') → h = h'
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : DiscreteTopology.{u_1} ↥H
hd : IsDiscrete (↑H : Set G)
V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
VH : V ∩ (↑H : Set G) = {1}
this : (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ (↑H : Set G)
h' : G
h'_in : h' ∈ (↑H : Set G)
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (h, h') → h = h'
have simp : h' * h⁻¹ ∈ V → h = h'
Tactic: simp only [Set.mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : DiscreteTopology.{u_1} ↥H
hd : IsDiscrete (↑H : Set G)
V : Set G
V_in : Membership.mem (γ := Filter G) (𝓝 1) V
VH : V ∩ (↑H : Set G) = {1}
this : (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ (↑H : Set G)
h' : G
h'_in : h' ∈ (↑H : Set G)
hyp : h' * h⁻¹ ∈ V
⊢ h = h'
have this₁ : Membership.mem (γ := Set G) {1} (h' * h⁻¹)
Tactic: have : h' * h⁻¹ ∈ ({1} : Set G) := VH ▸ Set.mem_inter hyp (H.mul_mem h'_in (H.inv_mem h_in))
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Type u_2
inst_4 : Group H
f : H →* G
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
hf' : IsDiscrete (↑f.range : Set G)
⊢ Tendsto.{u_2, u_1} (α := H) (⇑f : (a : H) → G) cofinite (cocompact G)
have hf₁ : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := ↥f.range) (⇑f.rangeRestrict : (a : H) → ↥f.range)
Tactic: replace hf : Function.Injective f.rangeRestrict := by simpa
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ UniformSpace.comap op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G
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
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ 𝓤 G = 𝓤 G
have h : Eq.{u_1 + 1} (α := Filter (G × G))
  (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
    (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.2 * p.1⁻¹) (𝓝 1)))
  (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))
Tactic: change comap (fun (x : G × G) ↦ (MulOpposite.op x.1, MulOpposite.op x.2))
      (comap (fun p : Gᵐᵒᵖ × Gᵐᵒᵖ => p.2 * p.1⁻¹) (𝓝 1))
    = comap (fun p : G × G => p.1⁻¹ * p.2) (𝓝 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
      (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.2 * p.1⁻¹) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))
have this : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (comap (β := Gᵐᵒᵖ) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) (𝓝 1))
Tactic: have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (comap (β := Gᵐᵒᵖ) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) (𝓝 1))
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
      (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.2 * p.1⁻¹) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))
have h : Eq.{u_1 + 1} (α := Filter (G × G))
  (comap (β := Gᵐᵒᵖ) ((fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.2 * p.1⁻¹) ∘ fun (x : G × G) ↦ (op x.1, op x.2)) (𝓝 1))
  (comap (β := Gᵐᵒᵖ) (Function.comp (β := G) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1))
Tactic: simp_rw [comap_comap, this, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ UniformSpace.comap op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G
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
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ 𝓤 G = 𝓤 G
have h : Eq.{u_1 + 1} (α := Filter (G × G))
  (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
    (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.1⁻¹ * p.2) (𝓝 1)))
  (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
Tactic: change comap (fun (x : G × G) ↦ (MulOpposite.op x.1, MulOpposite.op x.2))
      (comap (fun p : Gᵐᵒᵖ × Gᵐᵒᵖ => p.1⁻¹ * p.2) (𝓝 1))
    = comap (fun p : G × G => p.2 * p.1⁻¹) (𝓝 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
      (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.1⁻¹ * p.2) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
have this : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (comap (β := Gᵐᵒᵖ) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) (𝓝 1))
Tactic: have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (comap (β := Gᵐᵒᵖ) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) (𝓝 1))
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := Gᵐᵒᵖ × Gᵐᵒᵖ) (fun (x : G × G) ↦ (op x.1, op x.2))
      (comap (β := Gᵐᵒᵖ) (fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.1⁻¹ * p.2) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
have h : Eq.{u_1 + 1} (α := Filter (G × G))
  (comap (β := Gᵐᵒᵖ) ((fun (p : Gᵐᵒᵖ × Gᵐᵒᵖ) ↦ p.1⁻¹ * p.2) ∘ fun (x : G × G) ↦ (op x.1, op x.2)) (𝓝 1))
  (comap (β := Gᵐᵒᵖ) (Function.comp (β := G) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
Tactic: simp_rw [comap_comap, this, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : TopologicalSpace G_1
inst_2 : IsTopologicalGroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ G ≃ᵤ Gᵐᵒᵖ
have refine_1 : UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)
Tactic: refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : TopologicalSpace G_1
inst_2 : IsTopologicalGroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
this_1 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
refine_1 : UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)
⊢ G ≃ᵤ Gᵐᵒᵖ
have refine_2 : UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)
Tactic: refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : TopologicalSpace G_1
inst_2 : IsTopologicalGroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
this_1 : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
⊢ G ≃ᵤ Gᵐᵒᵖ
have refine_1 : UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)
Tactic: refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G_1 : Type u_1
inst : Group G_1
inst_1 : TopologicalSpace G_1
inst_2 : IsTopologicalGroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : IsTopologicalGroup G
this_1 : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
refine_1 : UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)
⊢ G ≃ᵤ Gᵐᵒᵖ
have refine_2 : UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)
Tactic: refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G) =
    IsTopologicalGroup.rightUniformSpace G
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
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq (α := Filter G) (𝓝 1) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))
have rw : Eq (α := Filter G) (𝓝 1 : Filter G) (𝓝 ((Homeomorph.symm (Homeomorph.inv G) : (a : G) → G) 1) : Filter G)
Tactic: rw [Homeomorph.comap_nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := G × G) (fun (x : G × G) ↦ ((Equiv.inv G : (a : G) → G) x.1, (Equiv.inv G : (a : G) → G) x.2))
      (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
have this : Eq (α := Filter G) (𝓝 1) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))
Tactic: have : 𝓝 (1 : G) = comap (Homeomorph.inv G) (𝓝 1) := by rw [Homeomorph.comap_nhds_eq]; simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this : Eq (α := Filter G) (𝓝 1) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))
⊢ Eq.{u_1 + 1} (α := Filter (G × G))
    (comap (β := G × G) (fun (x : G × G) ↦ ((Equiv.inv G : (a : G) → G) x.1, (Equiv.inv G : (a : G) → G) x.2))
      (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (𝓝 1)))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
have h : Eq (α := Filter (G × G))
  (comap (β := G × G) (fun (x : G × G) ↦ ((Equiv.inv G : (a : G) → G) x.1, (Equiv.inv G : (a : G) → G) x.2))
    (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))))
  (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
Tactic: nth_rewrite 1 [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this : Eq (α := Filter G) (𝓝 1) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))
⊢ Eq (α := Filter (G × G))
    (comap (β := G × G) (fun (x : G × G) ↦ ((Equiv.inv G : (a : G) → G) x.1, (Equiv.inv G : (a : G) → G) x.2))
      (comap (β := G) (fun (p : G × G) ↦ p.1⁻¹ * p.2) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))))
    (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
have h : Eq (α := Filter (G × G))
  (comap (β := G)
    (Function.comp (β := G) (⇑(Homeomorph.inv G) : (a : G) → G)
      ((fun (p : G × G) ↦ p.1⁻¹ * p.2) ∘ fun (x : G × G) ↦
        ((Equiv.inv G : (a : G) → G) x.1, (Equiv.inv G : (a : G) → G) x.2)))
    (𝓝 1))
  (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
Tactic: rw [comap_comap, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
have apply : IsTopologicalGroup.rightUniformSpace G ≤
  UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G)
Tactic: apply uniformContinuous_iff.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ IsTopologicalGroup.rightUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G)
have rw : LE.le (α := UniformSpace G) (UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G))
  (UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G))
Tactic: rw [← comap_inv_leftUniformSpace]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ G ≃ᵤ G
have A : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
Tactic: have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G)
      (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff.2
    rw [← comap_inv_leftUniformSpace]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
A : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
⊢ UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
have apply : IsTopologicalGroup.leftUniformSpace G ≤
  UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.rightUniformSpace G)
Tactic: apply uniformContinuous_iff.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
A : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.rightUniformSpace G)
have rw : IsTopologicalGroup.leftUniformSpace G ≤
  UniformSpace.comap (Function.comp (β := G) (⇑(Equiv.inv G) : (a : G) → G) (⇑(Equiv.inv G) : (a : G) → G))
    (IsTopologicalGroup.leftUniformSpace G)
Tactic: rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
A : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
⊢ G ≃ᵤ G
have B : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
Tactic: have B : @UniformContinuous G G (IsTopologicalGroup.leftUniformSpace G)
      (IsTopologicalGroup.rightUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff.2
    rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ UniformCauchySeqOn F p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a / F m.1 a ∈ u_1
have simp : UniformCauchySeqOn F p s ↔
  ∀ (u_1 : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a * (F m.1 a)⁻¹ ∈ u_1
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1
have simp : TendstoUniformly F f p ↔
  ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoUniformlyOn F f p s ↔
    ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a / f a ∈ u_1
have simp : TendstoUniformlyOn F f p s ↔
  ∀ (u_1 : Set G), Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ᶠ (i : ι) in p, ∀ a ∈ s, F i a * (f a)⁻¹ ∈ u_1
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1
have simp : TendstoLocallyUniformly F f p ↔
  ∀ (u_1 : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Group G
u : UniformSpace G
inst_1 : IsTopologicalGroup G
inst_2 : TopologicalSpace α
F : ι → α → G
f : α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (u_1 : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1
have simp : TendstoLocallyUniformlyOn F f p s ↔
  ∀ (u_1 : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) u_1 → ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a * (f a)⁻¹ ∈ u_1
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
⊢ Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
have h : ∀ (t : β × β),
  Eq.{u_1 + 1} (α := α)
    (((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2)) t)
    (comp (β := β) (⇑e : (a : β) → α) (fun (t : β × β) ↦ t.2 / t.1) t)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
⊢ Tendsto (β := β) (fun (t : β × β) ↦ t.2 / t.1)
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
have comm : Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
  (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
Tactic: have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) =
      e ∘ fun t : β × β => t.2 / t.1 := by
    ext t
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
hom : Type u_3
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : IsTopologicalGroup α
inst_3 : TopologicalSpace β
inst_4 : Group β
inst_5 : FunLike hom β α
inst_6 : MonoidHomClass hom β α
e : hom
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
x₀ : α
comm :
  Eq (α := β × β → α) ((fun (x : α × α) ↦ x.2 / x.1) ∘ fun (t : β × β) ↦ ((e : (a : β) → α) t.1, (e : (a : β) → α) t.2))
    (comp (β := β) (⇑e : (a : β) → α) fun (t : β × β) ↦ t.2 / t.1)
⊢ Tendsto (β := β) (fun (t : β × β) ↦ t.2 / t.1)
    (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
have lim : Tendsto (β := α) (fun (x : α × α) ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 ((e : (a : β) → α) 1) : Filter α)
Tactic: have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
    simpa using (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace δ
inst_6 : AddCommGroup δ
inst_7 : UniformSpace G
inst_8 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_7.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
⊢ Tendsto (β := β × δ) (fun (a : β × β) ↦ (a.2 - a.1, y₁))
    (SProd.sprod (α := Filter β) (β := Filter β) (comap (⇑e : (a : β) → α) Nx) (comap (⇑e : (a : β) → α) Nx))
    (𝓝 (0, y₁))
have this : Tendsto (fun (x : β × β) ↦ (x.2 - x.1, y₁))
  (comap (fun (p : β × β) ↦ ((e : (a : β) → α) p.1, (e : (a : β) → α) p.2)) (𝓝 (x₀, x₀)))
  (SProd.sprod (α := Filter β) (𝓝 0) (𝓝 y₁))
Tactic: have := Tendsto.prodMk (tendsto_sub_comap_self de x₀)
      (tendsto_const_nhds : Tendsto (fun _ : β × β => y₁) (comap ee <| 𝓝 (x₀, x₀)) (𝓝 y₁))