awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ CompleteSpace.{u} (G ⧸ N)
have hv₁ : 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
Cleared hypotheses: hv, v_anti
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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)
have refine : ∀ (x : ℕ → G ⧸ N) (hx : CauchySeq x), ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)
Tactic: refine UniformSpace.complete_of_cauchySeq_tendsto fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ ∀ (i j : ℕ),
    ∃ (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)
have 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)}
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 _
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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 j : ℕ),
    ∃ (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)
have 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)
Tactic: rw [h𝓤GN.cauchySeq_iff] at hx
Cleared hypotheses: hx, h𝓤GN
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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 j : ℕ),
    ∃ (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)
have hx₁ : ∀ (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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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 : ℕ),
    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)
have 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)
Tactic: rcases hx i with ⟨M, hM⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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)
have 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)
Tactic: refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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)
⊢ ∃ (g' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)
have 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)
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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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' : G), g / g' ∈ u i ∧ x a = (↑g' : G ⧸ N)
have simpa : x a = (↑(y⁻¹ * g) : G ⧸ N)
Tactic: refine
      ⟨y⁻¹ * g, by
        simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw₁ : x a = HMul.hMul (α := G ⧸ N) (↑y : G ⧸ N)⁻¹ (↑g : G ⧸ N)
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
rw₁ : x a = HMul.hMul (α := G ⧸ N) (↑y : G ⧸ N)⁻¹ (↑g : G ⧸ N)
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw₂ : x a = (x b / x a)⁻¹ * (↑g : G ⧸ N)
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
rw₁ : x a = HMul.hMul (α := G ⧸ N) (↑y : G ⧸ N)⁻¹ (↑g : G ⧸ N)
rw₂ : x a = (x b / x a)⁻¹ * (↑g : G ⧸ N)
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw₃ : x a = ((↑g : G ⧸ N) / x a)⁻¹ * (↑g : G ⧸ N)
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
rw₁ : x a = HMul.hMul (α := G ⧸ N) (↑y : G ⧸ N)⁻¹ (↑g : G ⧸ N)
rw₂ : x a = (x b / x a)⁻¹ * (↑g : G ⧸ N)
rw₃ : x a = ((↑g : G ⧸ N) / x a)⁻¹ * (↑g : G ⧸ N)
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw₄ : x a = x a / (↑g : G ⧸ N) * (↑g : G ⧸ N)
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
rw : x a = HMul.hMul (α := G ⧸ N) (↑y⁻¹ : G ⧸ N) (↑g : G ⧸ N)
rw₁ : x a = HMul.hMul (α := G ⧸ N) (↑y : G ⧸ N)⁻¹ (↑g : G ⧸ N)
rw₂ : x a = (x b / x a)⁻¹ * (↑g : G ⧸ N)
rw₃ : x a = ((↑g : G ⧸ N) / x a)⁻¹ * (↑g : G ⧸ N)
rw₄ : x a = x a / (↑g : G ⧸ N) * (↑g : G ⧸ N)
⊢ x a = (↑(y⁻¹ * g) : G ⧸ N)
have rw₅ : x a = x a
Tactic: rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)
have key₀ : ∀ (i j : ℕ),
  ∃ (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: have key₀ : ∀ i j : ℕ, ∃ M : ℕ, j < M ∧ ∀ a b : ℕ, M ≤ a → M ≤ b →
      ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u i ∧ x a = g' := by
    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 _
    rw [h𝓤GN.cauchySeq_iff] at hx
    simp only [mem_setOf_eq, forall_true_left, mem_image] at hx
    intro i j
    rcases hx i with ⟨M, hM⟩
    refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩
    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)
    refine
      ⟨y⁻¹ * g, by
        simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem, ?_⟩
    rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]