awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
U : Set β
V : Set δ
h :
  ∀ x ∈ U,
    ∀ x' ∈ U,
      ∀ y ∈ V,
        ∀ y' ∈ V,
          HSub.hSub (α := G)
              ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x', y'))
              ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x, y)) ∈
            W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : (⇑e : (a : β) → α) ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : (⇑f : (a : δ) → γ) ⁻¹' V' ⊆ V
⊢ U' ×ˢ V' ∈ 𝓝 x₀ ×ˢ 𝓝 y₀

Tactic:
have := prod_mem_prod U'_nhds V'_nhds
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst : TopologicalSpace α
inst_1 : AddCommGroup α
inst_2 : IsTopologicalAddGroup α
inst_3 : TopologicalSpace β
inst_4 : AddCommGroup β
inst_5 : TopologicalSpace γ
inst_6 : AddCommGroup γ
inst_7 : IsTopologicalAddGroup γ
inst_8 : TopologicalSpace δ
inst_9 : AddCommGroup δ
inst_10 : UniformSpace G
inst_11 : AddCommGroup G
e : β →+ α
de : IsDenseInducing.{u_2, u_1} (α := β) (β := α) (⇑e : (a : β) → α)
f : δ →+ γ
df : IsDenseInducing.{u_4, u_3} (α := δ) (β := γ) (⇑f : (a : δ) → γ)
φ : β →+ δ →+ G
hφ :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : β × δ) ↦
    (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2
inst_12 : IsUniformAddGroup G
inst_13 : T0Space G
inst_14 : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
U : Set β
V : Set δ
h :
  ∀ x ∈ U,
    ∀ x' ∈ U,
      ∀ y ∈ V,
        ∀ y' ∈ V,
          HSub.hSub (α := G)
              ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x', y'))
              ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x, y)) ∈
            W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : (⇑e : (a : β) → α) ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : (⇑f : (a : δ) → γ) ⁻¹' V' ⊆ V
this : U' ×ˢ V' ∈ 𝓝 x₀ ×ˢ 𝓝 y₀
⊢ (∃ t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀, t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    Subset (α := Set ((β × δ) × β × δ))
      ((fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2)) ⁻¹'
        (U' ×ˢ V') ×ˢ U' ×ˢ V')
      ((fun (p : (β × δ) × β × δ) ↦
          HSub.hSub (α := G) ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) p.2)
            ((fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) p.1)) ⁻¹'
        W')

Tactic:
grind
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))

Tactic:
haveI : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
obtain :
  ∀ (u : ℕ → Set G) (hu : HasAntitoneBasis (𝓝 1) u) (u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n),
    CompleteSpace.{u} (G ⧸ N)
⊢ CompleteSpace.{u} (G ⧸ N)

Tactic:
obtain ⟨u, hu, u_mul⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one G

Premises used: IsTopologicalGroup.exists_antitone_basis_nhds_one
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
⊢ HasBasis.{u, 1} (α := G ⧸ N) (Filter.map mk (𝓝 1)) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x

Tactic:
obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)

Premises used: QuotientGroup.mk, Filter.HasAntitoneBasis.map
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (Filter.map mk (𝓝 1)) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
⊢ Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x

Tactic:
obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)

Premises used: QuotientGroup.mk, Filter.HasAntitoneBasis.map
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (Filter.map mk (𝓝 1)) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
⊢ HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x

Tactic:
rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv

Premises used: QuotientGroup.mk_one, QuotientGroup.nhds_eq, OfNat.ofNat
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (Filter.map mk (𝓝 1)) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
hv₁ : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
⊢ Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x

Tactic:
rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv

Premises used: QuotientGroup.mk_one, QuotientGroup.nhds_eq, OfNat.ofNat
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
⊢ CompleteSpace.{u} (G ⧸ N)

Tactic:
UniformSpace.complete_of_cauchySeq_tendsto fun x hx => ?_

Premises used: UniformSpace.complete_of_cauchySeq_tendsto
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
refine : ∀ (x : ℕ → G ⧸ N) (hx : CauchySeq x), ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)
⊢ CompleteSpace.{u} (G ⧸ N)

Tactic:
refine UniformSpace.complete_of_cauchySeq_tendsto fun x hx => ?_

Premises used: UniformSpace.complete_of_cauchySeq_tendsto
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}

Tactic:
simpa [uniformity_eq_comap_nhds_one', div_eq_mul_inv] using hv.comap _

Premises used: div_eq_mul_inv, Filter.HasBasis.comap, uniformity_eq_comap_nhds_one'
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}

Tactic:
have h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun _ ↦ True) fun i ↦ { x | x.snd / x.fst ∈ (↑) '' u i } := by
      simpa [uniformity_eq_comap_nhds_one', div_eq_mul_inv] using hv.comap _
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
⊢ ∀ (i : ℕ),
    True →
      ∃ (N_1 : ℕ),
        ∀ (m : ℕ),
          N_1 ≤ m →
            ∀ (n : ℕ),
              N_1 ≤ n →
                Membership.mem (γ := SetRel (G ⧸ N) (G ⧸ N))
                  {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)} (x m, x n)

Tactic:
rw [h𝓤GN.cauchySeq_iff] at hx

Premises used: Filter.HasBasis.cauchySeq_iff
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx₁ :
  ∀ (i : ℕ),
    True →
      ∃ (N_1 : ℕ),
        ∀ (m : ℕ),
          N_1 ≤ m →
            ∀ (n : ℕ),
              N_1 ≤ n →
                Membership.mem (γ := SetRel (G ⧸ N) (G ⧸ N))
                  {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)} (x m, x n)
⊢ HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}

Tactic:
rw [h𝓤GN.cauchySeq_iff] at hx

Premises used: Filter.HasBasis.cauchySeq_iff
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
hx :
  ∀ (i : ℕ),
    True →
      ∃ (N_1 : ℕ),
        ∀ (m : ℕ),
          N_1 ≤ m →
            ∀ (n : ℕ),
              N_1 ≤ n →
                Membership.mem (γ := SetRel (G ⧸ N) (G ⧸ N))
                  {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)} (x m, x n)
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
⊢ ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m

Tactic:
simp only [mem_setOf_eq, forall_true_left, mem_image] at hx

Premises used: forall_true_left, Set.mem_image, Set.mem_setOf_eq
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx : ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
i j : ℕ
rcases :
  ∀ (M : ℕ) (hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m),
    ∃ (M : ℕ),
      j < M ∧
        ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)
⊢ ∃ (M : ℕ),
    j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)

Tactic:
rcases hx i with ⟨M, hM⟩
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx : ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
⊢ ∃ (M : ℕ),
    j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)

Tactic:
⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩

Premises used: lt_add_one, HAdd.hAdd, Max.max, And.intro, Exists.intro, OfNat.ofNat, le_max_left, LE.le.trans_lt
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx : ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
refine :
  ∀ (a b : ℕ) (ha : max j M + 1 ≤ a) (hb : max j M + 1 ≤ b) (g : G) (hg : x b = (↑g : G ⧸ N)),
    ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)
⊢ ∃ (M : ℕ),
    j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)

Tactic:
refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx : ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = (↑g : G ⧸ N)
obtain : ∀ (y : G) (y_mem : y ∈ u i) (hy : (↑y : G ⧸ N) = x b / x a), ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)
⊢ ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)

Tactic:
obtain ⟨y, y_mem, hy⟩ :=
      hM a (((le_max_right j _).trans (lt_add_one _).le).trans ha) b
        (((le_max_right j _).trans (lt_add_one _).le).trans hb)

Premises used: le_max_right, lt_add_one, LT.lt.le, LE.le.trans
-- 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
inst_5 : CompleteSpace G
this_1 : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this_2 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
u : ℕ → Set G
hu : HasAntitoneBasis (𝓝 1) u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : HasBasis.{u, 1} (α := G ⧸ N) (𝓝 1) (fun (x : ℕ) ↦ True) fun (x : ℕ) ↦ mk '' u x
v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN :
  HasBasis.{u, 1} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N)) (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦
    {x : (G ⧸ N) × G ⧸ N | Membership.mem (γ := Set (G ⧸ N)) (mk '' u i) (x.2 / x.1)}
hx : ∀ (i : ℕ), ∃ (N_1 : ℕ), ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, (↑x_1 : G ⧸ N) = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = (↑g : G ⧸ N)
y : G
y_mem : y ∈ u i
hy : (↑y : G ⧸ N) = x b / x a
⊢ g / (y⁻¹ * g) ∈ u i

Tactic:
simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem

Premises used: div_eq_mul_inv, inv_inv, mul_inv_rev, mul_inv_cancel_left