awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
rw :
  ∀ (hf : Tendsto (β := G) (fun (x : G × G) ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)) (this : f.NeBot) (K : Set G)
    (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K), ∃ (x : G), ∀ᶠ (y : G) in f, y / x ∈ K
⊢ ∃ (x : G), ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf

Premises used: Filter.tendsto_iff_comap, cauchy_iff_le, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Tendsto (β := G) (fun (x : G × G) ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
⊢ ∃ (x : G), ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
hf.eventually_mem K_mem |>.curry.exists

Premises used: Set.Mem, Filter.Eventually.curry, Filter.Tendsto.eventually_mem, Filter.Eventually.exists
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Tendsto (β := G) (fun (x : G × G) ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
⊢ ∃ (x : G), ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
exact hf.eventually_mem K_mem |>.curry.exists

Premises used: Filter.Eventually.curry, Filter.Tendsto.eventually_mem, Filter.Eventually.exists
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
obtain : ∀ (x : G) (hx : ∀ᶠ (y : G) in f, y / x ∈ K), ∃ (x : G), f ≤ 𝓝 x
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by
      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
      exact hf.eventually_mem K_mem |>.curry.exists
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y / x ∈ K
⊢ ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K

Tactic:
simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv,
      ← mem_smul_set_iff_inv_smul_mem] at hx

Premises used: op_smul_eq_mul, div_eq_mul_inv, Set.mem_smul_set_iff_inv_smul_mem, MulOpposite.op_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
⊢ IsComplete (MulOpposite.op x • K)

Tactic:
have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
⊢ f ≤ 𝓟 (MulOpposite.op x • K)

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
obtain : ∀ (l : G) (hl : f ≤ 𝓝 l), ∃ (x : G), f ≤ 𝓝 x
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
l : G
hl : f ≤ 𝓝 l
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
⟨l, hl⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : Membership.mem (γ := Filter G) (𝓝 1) K
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
l : G
hl : f ≤ 𝓝 l
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
exact ⟨l, hl⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
open open₁ open₂ : ∀ (this : f.NeBot), ∃ (x : G), f ≤ 𝓝 x
open₃ :
  ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K),
    ∃ (x : G), f ≤ 𝓝 x
open₄ :
  ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K) (x : G)
    (hx : ∀ᶠ (y : G) in f, y / x ∈ K), ∃ (x : G), f ≤ 𝓝 x
open₅ :
  ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K) (x : G)
    (hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K), ∃ (x : G), f ≤ 𝓝 x
open₆ :
  ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K) (x : G)
    (hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K) (Kx_complete : IsComplete (MulOpposite.op x • K)),
    ∃ (x : G), f ≤ 𝓝 x
open₇ :
  ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K) (x : G)
    (hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K) (Kx_complete : IsComplete (MulOpposite.op x • K)) (l : G)
    (hl : f ≤ 𝓝 l), ∃ (x : G), f ≤ 𝓝 x
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
open scoped RightActions in
    have : f.NeBot := hf.1
    obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by
      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
      exact hf.eventually_mem K_mem |>.curry.exists
    simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv,
      ← mem_smul_set_iff_inv_smul_mem] at hx
    have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete
    obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
    exact ⟨l, hl⟩

Premises used: op_smul_eq_mul, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, div_eq_mul_inv, Set.mem_smul_set_iff_inv_smul_mem, OfNat.ofNat, MulOpposite.op_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
S : Subgroup α
⊢ IsUniformGroup.{u_1} ↥S

Tactic:
.comap S.subtype

Premises used: Subgroup.subtype, IsUniformGroup.comap
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
inst_3 : Preorder ι
u v : ι → α
hu : CauchySeq u
hv : CauchySeq v
⊢ CauchySeq (u * v)

Tactic:
uniformContinuous_mul.comp_cauchySeq (hu.prodMk hv)

Premises used: uniformContinuous_mul, CauchySeq.prodMk, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
inst_3 : Preorder ι
u : ι → α
x : α
hu : CauchySeq u
⊢ CauchySeq.{u_1, u_3} (α := α) fun (n : ι) ↦ u n * x

Tactic:
(uniformContinuous_id.mul uniformContinuous_const).comp_cauchySeq hu

Premises used: uniformContinuous_id, uniformContinuous_const, UniformContinuous.mul, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
inst_3 : Preorder ι
u : ι → α
x : α
hu : CauchySeq u
⊢ CauchySeq.{u_1, u_3} (α := α) fun (n : ι) ↦ x * u n

Tactic:
(uniformContinuous_const.mul uniformContinuous_id).comp_cauchySeq hu

Premises used: uniformContinuous_id, uniformContinuous_const, UniformContinuous.mul, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
inst_3 : Preorder ι
u : ι → α
h : CauchySeq u
⊢ CauchySeq u⁻¹

Tactic:
uniformContinuous_inv.comp_cauchySeq h

Premises used: uniformContinuous_inv, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
s : Set α
⊢ (∀ (i : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) i →
        ∃ (t : Set α),
          t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | Membership.mem (γ := SetRel α α) {x : α × α | x.2⁻¹ * x.1 ∈ id i} (x, y)}) ↔
    ∀ (U : Set α), Membership.mem (γ := Filter α) (𝓝 1) U → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

Tactic:
simp [← preimage_smul_inv, preimage]

Premises used: Set.preimage_smul_inv, Set.preimage
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
s : Set α
hs : TotallyBounded s
⊢ TotallyBounded (α := α) ((fun (x : α) ↦ x⁻¹) '' s)

Tactic:
TotallyBounded.image hs uniformContinuous_inv

Premises used: TotallyBounded.image, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
s : Set α
hs : TotallyBounded s
h : Eq.{u_1 + 1} (α := Set α → Set α) Inv.inv (image fun (x : α) ↦ x⁻¹)
⊢ TotallyBounded s⁻¹

Tactic:
convert! TotallyBounded.image hs uniformContinuous_inv

Premises used: TotallyBounded.image, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
s : Set α
hs : TotallyBounded s
⊢ Eq.{u_1 + 1} (α := Set α → Set α) Inv.inv (image fun (x : α) ↦ x⁻¹)

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
l' : Filter β
f f' : ι → β → α
g g' : β → α
hf : TendstoUniformlyOnFilter f g l l'
hf' : TendstoUniformlyOnFilter f' g' l l'
⊢ TendstoUniformlyOnFilter (f * f') (g * g') l l'

Tactic:
fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformlyOnFilter (hf.prodMk hf')) u hu).diag_of_prod_left

Premises used: uniformContinuous_mul, Set.Mem, TendstoUniformlyOnFilter, TendstoUniformlyOnFilter.prodMk, UniformContinuous.comp_tendstoUniformlyOnFilter, Filter.Eventually.diag_of_prod_left
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
l' : Filter β
f f' : ι → β → α
g g' : β → α
hf : TendstoUniformlyOnFilter f g l l'
hf' : TendstoUniformlyOnFilter f' g' l l'
⊢ TendstoUniformlyOnFilter (f / f') (g / g') l l'

Tactic:
fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformlyOnFilter (hf.prodMk hf')) u hu).diag_of_prod_left

Premises used: Set.Mem, TendstoUniformlyOnFilter, TendstoUniformlyOnFilter.prodMk, uniformContinuous_div, UniformContinuous.comp_tendstoUniformlyOnFilter, Filter.Eventually.diag_of_prod_left
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
l' : Filter β
f : ι → β → α
g : β → α
hf : TendstoUniformlyOnFilter f g l l'
⊢ TendstoUniformlyOnFilter f⁻¹ g⁻¹ l l'

Tactic:
fun u hu ↦ uniformContinuous_inv.comp_tendstoUniformlyOnFilter hf u hu

Premises used: Set.Mem, TendstoUniformlyOnFilter, UniformContinuous.comp_tendstoUniformlyOnFilter, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
g g' : β → α
s : Set β
hf : TendstoUniformlyOn f g l s
hf' : TendstoUniformlyOn f' g' l s
⊢ TendstoUniformlyOn (f * f') (g * g') l s

Tactic:
fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformlyOn (hf.prodMk hf')) u hu).diag_of_prod

Premises used: Filter.Eventually.diag_of_prod, uniformContinuous_mul, Set.Mem, UniformContinuous.comp_tendstoUniformlyOn, TendstoUniformlyOn, TendstoUniformlyOn.prodMk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
g g' : β → α
s : Set β
hf : TendstoUniformlyOn f g l s
hf' : TendstoUniformlyOn f' g' l s
⊢ TendstoUniformlyOn (f / f') (g / g') l s

Tactic:
fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformlyOn (hf.prodMk hf')) u hu).diag_of_prod

Premises used: Filter.Eventually.diag_of_prod, Set.Mem, UniformContinuous.comp_tendstoUniformlyOn, TendstoUniformlyOn, uniformContinuous_div, TendstoUniformlyOn.prodMk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f : ι → β → α
g : β → α
s : Set β
hf : TendstoUniformlyOn f g l s
⊢ TendstoUniformlyOn f⁻¹ g⁻¹ l s

Tactic:
fun u hu ↦ uniformContinuous_inv.comp_tendstoUniformlyOn hf u hu

Premises used: Set.Mem, UniformContinuous.comp_tendstoUniformlyOn, TendstoUniformlyOn, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
g g' : β → α
hf : TendstoUniformly f g l
hf' : TendstoUniformly f' g' l
⊢ TendstoUniformly (f * f') (g * g') l

Tactic:
fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformly (hf.prodMk hf')) u hu).diag_of_prod

Premises used: Filter.Eventually.diag_of_prod, uniformContinuous_mul, Set.Mem, TendstoUniformly.prodMk, TendstoUniformly, UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
g g' : β → α
hf : TendstoUniformly f g l
hf' : TendstoUniformly f' g' l
⊢ TendstoUniformly (f / f') (g / g') l

Tactic:
fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformly (hf.prodMk hf')) u hu).diag_of_prod

Premises used: Filter.Eventually.diag_of_prod, Set.Mem, TendstoUniformly.prodMk, uniformContinuous_div, TendstoUniformly, UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f : ι → β → α
g : β → α
hf : TendstoUniformly f g l
⊢ TendstoUniformly f⁻¹ g⁻¹ l

Tactic:
fun u hu ↦ uniformContinuous_inv.comp_tendstoUniformly hf u hu

Premises used: Set.Mem, TendstoUniformly, uniformContinuous_inv, UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
hf' : UniformCauchySeqOn f' l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f * f') m.1 x, (f * f') m.2 x) ∈ u

Tactic:
simpa using (uniformContinuous_mul.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Premises used: uniformContinuous_mul, UniformCauchySeqOn.prod', UniformContinuous.comp_uniformCauchySeqOn
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
hf' : UniformCauchySeqOn f' l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f / f') m.1 x, (f / f') m.2 x) ∈ u

Tactic:
simpa using (uniformContinuous_div.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Premises used: UniformCauchySeqOn.prod', uniformContinuous_div, UniformContinuous.comp_uniformCauchySeqOn
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
l : Filter ι
f : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, (f⁻¹ m.1 x, f⁻¹ m.2 x) ∈ u

Tactic:
simpa using (uniformContinuous_inv.comp_uniformCauchySeqOn hf u hu)

Premises used: UniformContinuous.comp_uniformCauchySeqOn, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F G : ι → X → α
f g : X → α
s : Set X
l : Filter ι
hf : TendstoLocallyUniformlyOn F f l s
hg : TendstoLocallyUniformlyOn G g l s
⊢ TendstoLocallyUniformlyOn (F * G) (f * g) l s

Tactic:
uniformContinuous_mul.comp_tendstoLocallyUniformlyOn (hf.prodMk hg)

Premises used: uniformContinuous_mul, UniformContinuous.comp_tendstoLocallyUniformlyOn, TendstoLocallyUniformlyOn.prodMk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F G : ι → X → α
f g : X → α
s : Set X
l : Filter ι
hf : TendstoLocallyUniformlyOn F f l s
hg : TendstoLocallyUniformlyOn G g l s
⊢ TendstoLocallyUniformlyOn (F / G) (f / g) l s

Tactic:
uniformContinuous_div.comp_tendstoLocallyUniformlyOn (hf.prodMk hg)

Premises used: UniformContinuous.comp_tendstoLocallyUniformlyOn, uniformContinuous_div, TendstoLocallyUniformlyOn.prodMk
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F : ι → X → α
f : X → α
s : Set X
l : Filter ι
hf : TendstoLocallyUniformlyOn F f l s
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

Tactic:
uniformContinuous_inv.comp_tendstoLocallyUniformlyOn hf

Premises used: UniformContinuous.comp_tendstoLocallyUniformlyOn, uniformContinuous_inv
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F G : ι → X → α
f g : X → α
l : Filter ι
hf : TendstoLocallyUniformly F f l
hg : TendstoLocallyUniformly G g l
⊢ TendstoLocallyUniformly (F * G) (f * g) l

Tactic:
uniformContinuous_mul.comp_tendstoLocallyUniformly (hf.prodMk hg)

Premises used: uniformContinuous_mul, TendstoLocallyUniformly.prodMk, UniformContinuous.comp_tendstoLocallyUniformly
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F G : ι → X → α
f g : X → α
l : Filter ι
hf : TendstoLocallyUniformly F f l
hg : TendstoLocallyUniformly G g l
⊢ TendstoLocallyUniformly (F / G) (f / g) l

Tactic:
uniformContinuous_div.comp_tendstoLocallyUniformly (hf.prodMk hg)

Premises used: uniformContinuous_div, TendstoLocallyUniformly.prodMk, UniformContinuous.comp_tendstoLocallyUniformly
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
ι : Type u_3
X : Type u_4
inst_3 : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hf : TendstoLocallyUniformly F f l
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
uniformContinuous_inv.comp_tendstoLocallyUniformly hf

Premises used: UniformContinuous.comp_tendstoLocallyUniformly, uniformContinuous_inv
-- 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
⊢ IsDiscrete (↑H : Set G)

Tactic:
have hd : IsDiscrete (H : Set G) := isDiscrete_iff_discreteTopology.mpr ‹_›
-- 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), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑H : Set G) = {1}

Tactic:
nhds_inter_eq_singleton_of_mem_discrete hd H.one_mem

Premises used: nhds_inter_eq_singleton_of_mem_discrete, Subgroup.one_mem
-- 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)
obtain :
  ∀ (V : Set G) (V_in : Membership.mem (γ := Filter G) (𝓝 1) V) (VH : V ∩ (↑H : Set G) = {1}),
    IsClosed[inst_1] (↑H : Set G)
⊢ IsClosed[inst_1] (↑H : Set G)

Tactic:
obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = {1} :=
    nhds_inter_eq_singleton_of_mem_discrete hd H.one_mem

Premises used: nhds_inter_eq_singleton_of_mem_discrete, nhds, Subgroup.one_mem, SetLike.coe, OfNat.ofNat, Set
-- 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}
⊢ (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G

Tactic:
have : (fun p : G × G => p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_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 : (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
apply : (↑H : Set G).Pairwise fun (x y : G) ↦ (x, y) ∉ (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V
⊢ IsClosed[inst_1] (↑H : Set G)

Tactic:
apply isClosed_of_spaced_out this

Premises used: isClosed_of_spaced_out
-- 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)
contrapose : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) (h, h') → h = h'
⊢ h ≠ h' → (fun (x y : G) ↦ (x, y) ∉ (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'

Tactic:
contrapose