awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
⊢ -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
have rw : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * -(1 + x) + (↑this.unit⁻¹ : R) * 1
Tactic: rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
rw : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * -(1 + x) + (↑this.unit⁻¹ : R) * 1
⊢ -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
have rw₁ : -1 + (↑this.unit⁻¹ : R) = -((↑this.unit⁻¹ : R) * (1 + x)) + (↑this.unit⁻¹ : R) * 1
Tactic: rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
rw : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * -(1 + x) + (↑this.unit⁻¹ : R) * 1
rw₁ : -1 + (↑this.unit⁻¹ : R) = -((↑this.unit⁻¹ : R) * (1 + x)) + (↑this.unit⁻¹ : R) * 1
⊢ -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
have rw₂ : -1 + (↑this.unit⁻¹ : R) = -1 + (↑this.unit⁻¹ : R) * 1
Tactic: rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
rw : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * -(1 + x) + (↑this.unit⁻¹ : R) * 1
rw₁ : -1 + (↑this.unit⁻¹ : R) = -((↑this.unit⁻¹ : R) * (1 + x)) + (↑this.unit⁻¹ : R) * 1
rw₂ : -1 + (↑this.unit⁻¹ : R) = -1 + (↑this.unit⁻¹ : R) * 1
⊢ -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
have rw₃ : -1 + (↑this.unit⁻¹ : R) = -1 + (↑this.unit⁻¹ : R)
Tactic: rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
⊢ -1 + (↑this.unit⁻¹ : R) ∈ I ^ n
have this₁ : -1 + (↑this.unit⁻¹ : R) = -(↑this.unit⁻¹ : R) * x
Tactic: have : -1 + ↑this.unit⁻¹ = -this.unit⁻¹ * x := by
    trans this.unit⁻¹ * (-(1 + x) + 1)
    · rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
    · simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this_3 : IsUnit (1 + x)
this : -1 + (↑this_3.unit⁻¹ : R) = -(↑this_3.unit⁻¹ : R) * x
⊢ -1 + (↑this_3.unit⁻¹ : R) ∈ I ^ n
have rw : -(↑this_3.unit⁻¹ : R) * x ∈ I ^ n
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
⊢ comap (fun (x : α × α) ↦ (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α
have nth_rw : Function.Injective (β := α × α) fun (x : α × α) ↦ (x.1 * a, x.2 * a)
Tactic: nth_rw 1 [← uniformity_translate_mul a, comap_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have this : f.NeBot
Tactic: have : f.NeBot := hf.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have obtain : ∀ (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K), ∃ (x : G), f ≤ 𝓝 x
Tactic: obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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), ∀ᶠ (y : G) in f, y / x ∈ K
have 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
Tactic: rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
Cleared hypotheses: hf, this, K, K_compact, K_mem
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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), f ≤ 𝓝 x
have obtain : ∀ (x : G) (hx : ∀ᶠ (y : G) in f, y / x ∈ K), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have hx₁ : ∀ᶠ (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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have Kx_complete : IsComplete (MulOpposite.op x • K)
Tactic: have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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)
⊢ ∃ (x : G), f ≤ 𝓝 x
have obtain : ∀ (l : G) (hl : f ≤ 𝓝 l), ∃ (x : G), f ≤ 𝓝 x
Tactic: obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have open : ∀ (this : f.NeBot), ∃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have open₃ : ∀ (this : f.NeBot) (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K),
  ∃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ (x : G), f ≤ 𝓝 x
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
s : Set α
hs : TotallyBounded s
⊢ TotallyBounded s⁻¹
have h : Eq.{u_1 + 1} (α := Set α → Set α) Inv.inv (image fun (x : α) ↦ x⁻¹)
Tactic: convert! TotallyBounded.image hs uniformContinuous_inv
-- 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
⊢ IsClosed[inst_1] (↑H : Set G)
have hd : IsDiscrete (↑H : Set G)
Tactic: have hd : IsDiscrete (H : Set G) := isDiscrete_iff_discreteTopology.mpr ‹_›
-- 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)
⊢ IsClosed[inst_1] (↑H : Set G)
have obtain : ∀ (V : Set G) (V_in : Membership.mem (γ := Filter G) (𝓝 1) V) (VH : V ∩ (↑H : Set G) = {1}),
  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
-- 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}
⊢ IsClosed[inst_1] (↑H : Set G)
have this : (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
-- 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
⊢ IsClosed[inst_1] (↑H : Set G)
have apply : (↑H : Set G).Pairwise fun (x y : G) ↦ (x, y) ∉ (fun (p : G × G) ↦ p.2 * p.1⁻¹) ⁻¹' V
Tactic: apply isClosed_of_spaced_out this