awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
h : 𝓤 G = 𝓤 G
⊢ IsTopologicalGroup.rightUniformSpace G = us

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
h : 𝓤 G = comap (β := G) (fun (x : G × G) ↦ x.2 * x.1⁻¹) (𝓝 1)
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]

Premises used: IsRightUniformGroup.uniformity_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
⊢ 𝓤 G = comap (β := G) (fun (x : G × G) ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
⊢ IsTopologicalGroup.rightUniformSpace G = us

Tactic:
have : IsTopologicalGroup.rightUniformSpace G = us := by
    ext : 1
    rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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 G

Tactic:
rw [← this] at hG
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
hG₁ : CompleteSpace G
⊢ IsTopologicalGroup.rightUniformSpace G = us

Tactic:
rw [← this] at hG
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
rw : ∀ (hG : CompleteSpace G), CompleteSpace.{u} (G ⧸ N)
⊢ CompleteSpace.{u} (G ⧸ N)

Tactic:
rw [← IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace] at hG ⊢

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

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
h : 𝓤 G = 𝓤 G
⊢ IsTopologicalGroup.leftUniformSpace G = us

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
h : 𝓤 G = comap (β := G) (fun (x : G × G) ↦ x.1⁻¹ * x.2) (𝓝 1)
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]

Premises used: IsLeftUniformGroup.uniformity_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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 = comap (β := G) (fun (x : G × G) ↦ x.1⁻¹ * x.2) (𝓝 1)

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

Tactic:
have : IsTopologicalGroup.leftUniformSpace G = us := by
    ext : 1
    rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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 G

Tactic:
rw [← this] at hG
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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
hG₁ : CompleteSpace G
⊢ IsTopologicalGroup.leftUniformSpace G = us

Tactic:
rw [← this] at hG
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
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)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
us : Set (UniformSpace G)
h : ∀ u ∈ us, IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
@IsUniformGroup.mk G (_) _ <|
    uniformContinuous_sInf_rng.mpr fun u hu =>
      uniformContinuous_sInf_dom₂ hu hu (@IsUniformGroup.uniformContinuous_div G u _ (h u hu))

Premises used: Iff.mpr, uniformContinuous_sInf_rng, IsUniformGroup.uniformContinuous_div, uniformContinuous_sInf_dom₂, IsUniformGroup.mk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
isUniformGroup_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, isUniformGroup_sInf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
exact isUniformGroup_sInf (Set.forall_mem_range.mpr h')

Premises used: Iff.mpr, Set.forall_mem_range, isUniformGroup_sInf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
rw : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
isUniformGroup_iInf fun b => ?_

Premises used: isUniformGroup_iInf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
refine : ∀ (b : Bool), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
refine isUniformGroup_iInf fun b => ?_

Premises used: isUniformGroup_iInf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
b : Bool
false : IsUniformGroup G
true : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
inst : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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)
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)
⊢ UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2

Tactic:
simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]

Premises used: Function.comp_def, IsUniformInducing.uniformContinuous_iff, map_div
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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.{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:
uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

Premises used: UniformContinuous.prodMap, UniformContinuous.comp, uniformContinuous_div, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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.{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:
exact uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

Premises used: UniformContinuous.prodMap, UniformContinuous.comp, uniformContinuous_div, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
H : Type u_2
hom : Type u_3
inst : Group G
inst_1 : Group H
u : UniformSpace H
inst_2 : IsUniformGroup H
inst_3 : FunLike hom G H
inst_4 : MonoidHomClass hom G H
f : hom
⊢ IsUniformGroup G

Tactic:
letI : UniformSpace G := u.comap f; IsUniformInducing.isUniformGroup f ⟨rfl⟩

Premises used: IsUniformInducing.isUniformGroup, IsUniformInducing.mk, rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
H : Type u_2
hom : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : UniformSpace G
hG : IsUniformGroup G
inst_3 : UniformSpace H
hH : IsUniformGroup H
⊢ IsUniformGroup (G × H)

Tactic:
isUniformGroup_inf (.comap <| MonoidHom.fst G H) (.comap <| MonoidHom.snd G H)

Premises used: isUniformGroup_inf, Set.Mem, setOf, IsUniformGroup.comap, MonoidHom.fst, MonoidHom.snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Goal:
G : Type u_1
H : Type u_2
hom : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : UniformSpace G
hG : IsUniformGroup G
inst_3 : UniformSpace H
hH : IsUniformGroup H
⊢ IsUniformGroup (G × H)

Tactic:
exact isUniformGroup_inf (.comap <| MonoidHom.fst G H) (.comap <| MonoidHom.snd G H)

Premises used: isUniformGroup_inf, IsUniformGroup.comap, MonoidHom.fst, MonoidHom.snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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)
rw : IsUniformGroup ((i : ι) → G i)
⊢ IsUniformGroup ((i : ι) → G i)

Tactic:
rw [Pi.uniformSpace_eq]

Premises used: Pi.uniformSpace_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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)

Tactic:
isUniformGroup_iInf fun i ↦ .comap (Pi.evalMonoidHom G i)

Premises used: IsUniformGroup.comap, isUniformGroup_iInf, Pi.evalMonoidHom
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions
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)

Tactic:
exact isUniformGroup_iInf fun i ↦ .comap (Pi.evalMonoidHom G i)

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

Tactic:
IsRightUniformGroup.uniformity_eq

Premises used: IsRightUniformGroup.uniformity_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gₗ : Type u_2
inst : UniformSpace Gₗ
inst_1 : Group Gₗ
inst_2 : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (β := Gₗ) (fun (x : Gₗ × Gₗ) ↦ x.1⁻¹ * x.2) (𝓝 1)

Tactic:
IsLeftUniformGroup.uniformity_eq

Premises used: IsLeftUniformGroup.uniformity_eq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
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))
⊢ 𝓤 Gᵣ = 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]

Premises used: uniformity_eq_comap_mul_inv_nhds_one, Function.comp_def, Filter.comap_comap, comap_swap_uniformity
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
⊢ 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:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gₗ : Type u_2
inst : UniformSpace Gₗ
inst_1 : Group Gₗ
inst_2 : IsLeftUniformGroup Gₗ
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))
⊢ 𝓤 Gₗ = 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]

Premises used: uniformity_eq_comap_inv_mul_nhds_one, Function.comp_def, Filter.comap_comap, comap_swap_uniformity
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gₗ : Type u_2
inst : UniformSpace Gₗ
inst_1 : Group Gₗ
inst_2 : IsLeftUniformGroup Gₗ
⊢ 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:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
simp_rw : 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.2 * x.1⁻¹) (𝓝 1)
⊢ 𝓤 Gᵣ = comap (β := Gᵣ) (fun (x : Gᵣ × Gᵣ) ↦ x.2 / x.1) (𝓝 1)

Tactic:
simp_rw [div_eq_mul_inv]

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

Tactic:
uniformity_eq_comap_mul_inv_nhds_one Gᵣ

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

Tactic:
exact uniformity_eq_comap_mul_inv_nhds_one Gᵣ

Premises used: uniformity_eq_comap_mul_inv_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
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))
⊢ 𝓤 Gᵣ = 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]

Premises used: Function.comp_def, Filter.comap_comap, comap_swap_uniformity, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
Gᵣ : Type u_3
inst : UniformSpace Gᵣ
inst_1 : Group Gᵣ
inst_2 : IsRightUniformGroup Gᵣ
⊢ 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:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : Group α
h₁ : UniformContinuous (β := α) fun (p : α × α) ↦ p.1 * p.2
h₂ : UniformContinuous (β := α) fun (p : α) ↦ p⁻¹
⊢ UniformContinuous (β := α) fun (p : α × α) ↦ p.1 / p.2

Tactic:
simpa only [div_eq_mul_inv] using
    h₁.comp (uniformContinuous_fst.prodMk (h₂.comp uniformContinuous_snd))

Premises used: UniformContinuous.prodMk, uniformContinuous_snd, div_eq_mul_inv, UniformContinuous.comp, uniformContinuous_fst
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ UniformContinuous (β := α) fun (p : α × α) ↦ p.1 / p.2

Tactic:
IsUniformGroup.uniformContinuous_div

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

Tactic:
uniformContinuous_div.comp (hf.prodMk hg)

Premises used: UniformContinuous.prodMk, UniformContinuous.comp, uniformContinuous_div
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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 : β) ↦ 1 / f x

Tactic:
have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ 1 / f x
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ (f x)⁻¹

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ UniformContinuous (β := α) fun (x : α) ↦ x⁻¹

Tactic:
uniformContinuous_id.inv

Premises used: UniformContinuous.inv, uniformContinuous_id
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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)⁻¹

Tactic:
have : UniformContinuous fun x => f x / (g x)⁻¹ := hf.div hg.inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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
this : UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x / (g x)⁻¹
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_3
β : Type u_4
ι : Type u_5
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : ι → β → α
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → UniformContinuous (f i)
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ ∅, f i x

Tactic:
simpa using uniformContinuous_const

Premises used: uniformContinuous_const
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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 (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)

Tactic:
simp_rw [Finset.mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, Finset.mem_cons
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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 : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ cons a s ha, f i x

Tactic:
simpa [Finset.prod_cons] using h.1.mul (ih h.2)

Premises used: And.right, And.left, Finset.prod_cons, UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
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
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 ∈ Finset.cons a s ha, UniformContinuous (f i)),
    UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ Finset.cons a s ha, f i x
⊢ UniformContinuous.{u_4, u_3} (β := α) fun (x : β) ↦ ∏ i ∈ s, 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)

Premises used: Finset.cons, forall_eq_or_imp, uniformContinuous_const, Finset.prod_cons, Finset.mem_cons
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
⊢ UniformContinuous (β := α) fun (p : α × α) ↦ p.1 * p.2

Tactic:
uniformContinuous_fst.mul uniformContinuous_snd

Premises used: uniformContinuous_snd, uniformContinuous_fst, UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
a : α
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ f x * a

Tactic:
hf.mul uniformContinuous_const

Premises used: uniformContinuous_const, UniformContinuous.mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
inst_3 : UniformSpace β
f : β → α
hf : UniformContinuous f
a : α
⊢ UniformContinuous.{u_2, u_1} (β := α) fun (x : β) ↦ a * f x

Tactic:
uniformContinuous_const.mul hf

Premises used: uniformContinuous_const, UniformContinuous.mul