awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
simp : h' * h⁻¹ ∈ V → h = h'
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (h, h') → h = h'

Tactic:
simp only [Set.mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
⊢ 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))
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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_1 : (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
this : Membership.mem (γ := Set G) {1} (h' * h⁻¹)
⊢ h = h'

Tactic:
(eq_of_mul_inv_eq_one this).symm

Premises used: eq_of_mul_inv_eq_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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_1 : (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
this : Membership.mem (γ := Set G) {1} (h' * h⁻¹)
⊢ h = h'

Tactic:
exact (eq_of_mul_inv_eq_one this).symm

Premises used: eq_of_mul_inv_eq_one, Eq.symm
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
hH : IsDiscrete (↑H : Set G)
⊢ Tendsto (α := ↥H) (Subtype.val (p := fun (x : G) ↦ x ∈ H)) cofinite (cocompact G)

Tactic:
haveI : DiscreteTopology H := isDiscrete_iff_discreteTopology.mp hH
 IsClosed.tendsto_coe_cofinite_of_isDiscrete isClosed_of_discrete hH

Premises used: IsClosed.tendsto_coe_cofinite_of_isDiscrete, Subgroup.isClosed_of_discrete
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
⊢ Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := ↥f.range) (⇑f.rangeRestrict : (a : H) → ↥f.range)

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
⊢ 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
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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' : IsDiscrete (↑f.range : Set G)
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := ↥f.range) (⇑f.rangeRestrict : (a : H) → ↥f.range)
⊢ Tendsto.{u_2, u_1} (α := H) (⇑f : (a : H) → G) cofinite (cocompact G)

Tactic:
(f.range.tendsto_coe_cofinite_of_discrete hf').comp hf.tendsto_cofinite

Premises used: MonoidHom.range, Subgroup.tendsto_coe_cofinite_of_discrete, Function.Injective.tendsto_cofinite, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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' : IsDiscrete (↑f.range : Set G)
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := ↥f.range) (⇑f.rangeRestrict : (a : H) → ↥f.range)
⊢ Tendsto.{u_2, u_1} (α := H) (⇑f : (a : H) → G) cofinite (cocompact G)

Tactic:
exact (f.range.tendsto_coe_cofinite_of_discrete hf').comp hf.tendsto_cofinite

Premises used: MonoidHom.range, Subgroup.tendsto_coe_cofinite_of_discrete, Function.Injective.tendsto_cofinite, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
h : 𝓤 G = 𝓤 G
⊢ UniformSpace.comap op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
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))
⊢ 𝓤 G = 𝓤 G

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)

Premises used: HMul.hMul, nhds, Prod.mk, Prod.fst, Inv.inv, OfNat.ofNat, Prod.snd, Filter.comap, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (comap (β := Gᵐᵒᵖ) (⇑opHomeomorph : (a : G) → Gᵐᵒᵖ) (𝓝 1))

Tactic:
simp [Homeomorph.comap_nhds_eq]

Premises used: Homeomorph.comap_nhds_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ 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]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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))
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))
⊢ 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:
simp_rw [comap_comap, this, comap_comap]

Premises used: Filter.comap_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ) ((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:
rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
h : 𝓤 G = 𝓤 G
⊢ UniformSpace.comap op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
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))
⊢ 𝓤 G = 𝓤 G

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)

Premises used: HMul.hMul, nhds, Prod.mk, Prod.fst, Inv.inv, OfNat.ofNat, Prod.snd, Filter.comap, MulOpposite.op
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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))
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))
⊢ 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:
simp_rw [comap_comap, this, comap_comap]

Premises used: Filter.comap_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ) ((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:
rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
refine_2 : UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)
⊢ G ≃ᵤ Gᵐᵒᵖ

Tactic:
refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ
⊢ UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)

Tactic:
simp [uniformContinuous_iff, ← comap_op_leftUniformSpace]

Premises used: uniformContinuous_iff, MulOpposite.comap_op_leftUniformSpace
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ
⊢ UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)

Tactic:
simp [uniformContinuous_iff, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap]

Premises used: UniformSpace.comap_comap, uniformContinuous_iff, MulOpposite.comap_op_leftUniformSpace
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
refine_2 : UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)
⊢ G ≃ᵤ Gᵐᵒᵖ

Tactic:
refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ
⊢ UniformContinuous.{u_2, u_2} (α := G) (Equiv.toFun opEquiv)

Tactic:
simp [uniformContinuous_iff, ← comap_op_rightUniformSpace]

Premises used: uniformContinuous_iff, MulOpposite.comap_op_rightUniformSpace
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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ᵐᵒᵖ
⊢ UniformContinuous.{u_2, u_2} (α := Gᵐᵒᵖ) (Equiv.invFun opEquiv)

Tactic:
simp [uniformContinuous_iff, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]

Premises used: UniformSpace.comap_comap, uniformContinuous_iff, MulOpposite.comap_op_rightUniformSpace
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
h : 𝓤 G = 𝓤 G
⊢ UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G) =
    IsTopologicalGroup.rightUniformSpace G

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
rw : Eq (α := Filter G) (𝓝 1 : Filter G) (𝓝 ((Homeomorph.symm (Homeomorph.inv G) : (a : G) → G) 1) : Filter G)
⊢ Eq (α := Filter G) (𝓝 1) (comap (β := G) (⇑(Homeomorph.inv G) : (a : G) → G) (𝓝 1))

Tactic:
rw [Homeomorph.comap_nhds_eq]

Premises used: Homeomorph.comap_nhds_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq (α := Filter G) (𝓝 1 : Filter G) (𝓝 ((Homeomorph.symm (Homeomorph.inv G) : (a : G) → G) 1) : Filter G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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))

Tactic:
have : 𝓝 (1 : G) = comap (Homeomorph.inv G) (𝓝 1) := by rw [Homeomorph.comap_nhds_eq]; simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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))
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))
⊢ 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))

Tactic:
nth_rewrite 1 [this]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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))
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))
⊢ 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:
rw [comap_comap, comap_comap]

Premises used: Filter.comap_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
      (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:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
apply :
  IsTopologicalGroup.rightUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G)
⊢ UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)

Tactic:
apply uniformContinuous_iff.2

Premises used: Iff.mpr, uniformContinuous_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
rw 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))
⊢ IsTopologicalGroup.rightUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.leftUniformSpace G)

Tactic:
rw [← comap_inv_leftUniformSpace]

Premises used: comap_inv_leftUniformSpace
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)

Tactic:
have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G)
      (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by
    apply uniformContinuous_iff.2
    rw [← comap_inv_leftUniformSpace]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
apply :
  IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.rightUniformSpace G)
⊢ UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)

Tactic:
apply uniformContinuous_iff.2

Premises used: Iff.mpr, uniformContinuous_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
rw :
  IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (Function.comp (β := G) (⇑(Equiv.inv G) : (a : G) → G) (⇑(Equiv.inv G) : (a : G) → G))
      (IsTopologicalGroup.leftUniformSpace G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) : (a : G) → G) (IsTopologicalGroup.rightUniformSpace G)

Tactic:
rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]

Premises used: comap_inv_leftUniformSpace, UniformSpace.comap_comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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 (Function.comp (β := G) (⇑(Equiv.inv G) : (a : G) → G) (⇑(Equiv.inv G) : (a : G) → G))
      (IsTopologicalGroup.leftUniformSpace G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)

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
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)
B : UniformContinuous (α := G) (β := G) (⇑(Equiv.inv G) : (a : G) → G)
⊢ G ≃ᵤ G

Tactic:
exact @UniformEquiv.mk G G (IsTopologicalGroup.rightUniformSpace G)
    (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) A B

Premises used: Equiv.inv, UniformEquiv.mk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ CompleteSpace G ↔ CompleteSpace G

Tactic:
@UniformEquiv.completeSpace_iff G G (IsTopologicalGroup.rightUniformSpace G)
    (IsTopologicalGroup.leftUniformSpace G) (UniformEquiv.inv G)

Premises used: UniformEquiv.inv, UniformEquiv.completeSpace_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
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
⊢ 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]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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

Tactic:
hu ▸ ⟨fun h u hu ↦ h _ ⟨u, hu, fun _ ↦ id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩

Premises used: HMul.hMul, SProd.sprod, Filter.Eventually, Eq.rec, id, Prod.fst, Inv.inv, Set.preimage, And.intro, Iff.intro, Exists.intro, _private.0.IsTopologicalGroup.uniformCauchySeqOn_iff.match_1, Prod.snd, Filter.mem_of_superset