awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
⊢ CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))

Tactic:
have x'_cauchy : CauchySeq fun n => (x' n).fst := by
    have h𝓤G : (𝓤 G).HasBasis (fun _ => True) fun i => { x | x.snd / x.fst ∈ u i } := by
      simpa [uniformity_eq_comap_nhds_one', div_eq_mul_inv] using hu.toHasBasis.comap _
    rw [h𝓤G.cauchySeq_iff']
    simp only [mem_setOf_eq, forall_true_left]
    exact fun m =>
      ⟨m, fun n hmn =>
        Nat.decreasingInduction'
          (fun k _ _ hk => u_mul k ⟨_, hx' k, _, hk, div_mul_div_cancel _ _ _⟩) hmn
          (by simpa only [div_self'] using mem_of_mem_nhds (hu.mem _))⟩
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
rcases :
  ∀ (x₀ : G) (hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)),
    ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)
⊢ ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)

Tactic:
rcases cauchySeq_tendsto_of_complete x'_cauchy with ⟨x₀, hx₀⟩

Premises used: cauchySeq_tendsto_of_complete
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
⊢ ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)

Tactic:
⟨↑x₀,
      tendsto_nhds_of_cauchySeq_of_subseq hx
        (strictMono_nat_of_lt_succ fun n => (hφ (n + 1)).1).tendsto_atTop ?_⟩

Premises used: strictMono_nat_of_lt_succ, QuotientGroup.mk, StrictMono.tendsto_atTop, tendsto_nhds_of_cauchySeq_of_subseq, And.left, HAdd.hAdd, Exists.intro, 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
x : ℕ → G ⧸ N
hx : CauchySeq x
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
tendsto_nhds_of_cauchySeq_of_subseq : Tendsto (α := ℕ) (x ∘ fun (n : ℕ) ↦ φ (n + 1)) atTop (𝓝 (↑x₀ : G ⧸ N))
⊢ ∃ (a : G ⧸ N), Tendsto x atTop (𝓝 a)

Tactic:
refine
    ⟨↑x₀,
      tendsto_nhds_of_cauchySeq_of_subseq hx
        (strictMono_nat_of_lt_succ fun n => (hφ (n + 1)).1).tendsto_atTop ?_⟩
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
⊢ Tendsto (α := ℕ) (β := G ⧸ N) (mk ∘ fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop
    (𝓝 (↑x₀ : G ⧸ N))

Tactic:
((continuous_coinduced_rng : Continuous ((↑) : G → G ⧸ N)).tendsto x₀).comp hx₀

Premises used: Continuous.tendsto, Filter.Tendsto.comp, continuous_coinduced_rng
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
h :
  Eq (α := ℕ → G ⧸ N) (x ∘ fun (n : ℕ) ↦ φ (n + 1))
    (mk ∘ fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)))
⊢ Tendsto (α := ℕ) (x ∘ fun (n : ℕ) ↦ φ (n + 1)) atTop (𝓝 (↑x₀ : G ⧸ N))

Tactic:
convert! ((continuous_coinduced_rng : Continuous ((↑) : G → G ⧸ N)).tendsto x₀).comp hx₀

Premises used: Continuous.tendsto, Filter.Tendsto.comp, continuous_coinduced_rng
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
⊢ Eq (α := ℕ → G ⧸ N) (x ∘ fun (n : ℕ) ↦ φ (n + 1))
    (mk ∘ fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)))

Tactic:
funext fun n => (x' n).snd

Premises used: PSigma.snd, funext
-- 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
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)
φ : ℕ → ℕ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n
      (Classical.choose (p := fun (x_1 : ℕ) ↦
        0 < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u 0 ∧ x a = (↑g' : G ⧸ N))
        ⋯)
      fun (k yk : ℕ) ↦
      Classical.choose (p := fun (x_1 : ℕ) ↦
        yk < x_1 ∧
          ∀ (a b : ℕ),
            x_1 ≤ a → x_1 ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (k + 1) ∧ x a = (↑g' : G ⧸ N))
        ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ),
        φ (n + 1) ≤ a →
          φ (n + 1) ≤ b → ∀ (g : G), x b = (↑g : G ⧸ N) → ∃ (g' : G), g / g' ∈ u (n + 1) ∧ x a = (↑g' : G ⧸ N)
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = (↑g : G ⧸ N) :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x_1 : ℕ) ↦ (g : G) ×' x (φ (x_1 + 1)) = (↑g : G ⧸ N)) n
      (PSigma.mk (β := fun (g : G) ↦ x (φ (Nat.zero + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦ (↑x_1 : G ⧸ N) = x (φ 1)) ⋯) ⋯)
      fun (k : ℕ) (hk : (g : G) ×' x (φ (k + 1)) = (↑g : G ⧸ N)) ↦
      PSigma.mk (β := fun (g : G) ↦ x (φ (k.succ + 1)) = (↑g : G ⧸ N))
        (Classical.choose (p := fun (x_1 : G) ↦
          hk.fst (β := fun (g : G) ↦ x (φ (k + 1)) = (↑g : G ⧸ N)) / x_1 ∈ u (k + 1) ∧
            x (φ (k + 1 + 1)) = (↑x_1 : G ⧸ N))
          ⋯)
        ⋯
hx' :
  ∀ (n : ℕ),
    (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)) /
        PSigma.fst (β := fun (g : G) ↦ x (φ (n + 1 + 1)) = (↑g : G ⧸ N))
          (x' (n + 1) : (g : G) ×' x (φ (n + 1 + 1)) = (↑g : G ⧸ N)) ∈
      u (n + 1)
x'_cauchy : CauchySeq.{u, 0} (α := G) fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))
x₀ : G
hx₀ : Tendsto (fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N))) atTop (𝓝 x₀)
⊢ Eq (α := ℕ → G ⧸ N) (x ∘ fun (n : ℕ) ↦ φ (n + 1))
    (mk ∘ fun (n : ℕ) ↦ (x' n).fst (β := fun (g : G) ↦ x (φ (n + 1)) = (↑g : G ⧸ N)))

Tactic:
exact funext fun n => (x' n).snd

Premises used: PSigma.snd, funext