awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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 β
U_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U
V : Set δ
V_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V
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'
⊢ Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
have right : ∀ (U_nhds : ∃ t ∈ 𝓝 x₀, (⇑e : (a : β) → α) ⁻¹' t ⊆ U) (V : Set δ)
  (V_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V)
  (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'),
  Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
Tactic: rw [mem_comap] at U_nhds
Cleared hypotheses: U_nhds, V, V_nhds, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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 β
U_nhds : ∃ t ∈ 𝓝 x₀, (⇑e : (a : β) → α) ⁻¹' t ⊆ U
V : Set δ
V_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V
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'
⊢ Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
have right : ∀ (U' : Set α) (U'_nhds : U' ∈ 𝓝 x₀) (U'_sub : (⇑e : (a : β) → α) ⁻¹' U' ⊆ U),
  Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
Tactic: rcases U_nhds with ⟨U', U'_nhds, U'_sub⟩
Cleared hypotheses: U_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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 δ
V_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V
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
⊢ Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
have right : ∀ (V_nhds : ∃ t ∈ 𝓝 y₀, (⇑f : (a : δ) → γ) ⁻¹' t ⊆ V)
  (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),
  Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
Tactic: rw [mem_comap] at V_nhds
Cleared hypotheses: V_nhds, h, U', U'_nhds, U'_sub
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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 δ
V_nhds : ∃ t ∈ 𝓝 y₀, (⇑f : (a : δ) → γ) ⁻¹' t ⊆ V
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
⊢ Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
have right : ∀ (V' : Set γ) (V'_nhds : V' ∈ 𝓝 y₀) (V'_sub : (⇑f : (a : δ) → γ) ⁻¹' V' ⊆ V),
  Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
Tactic: rcases V_nhds with ⟨V', V'_nhds, V'_sub⟩
Cleared hypotheses: V_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ Membership.mem (γ := Filter G)
    (map
      (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))
      (comap
        (fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))))
    W'
have right : ∃ t ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀,
  Subset (α := Set ((β × δ) × β × δ))
    ((fun (p : (β × δ) × β × δ) ↦
        (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2)) ⁻¹'
      t)
    ((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: rw [mem_map, mem_comap, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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
⊢ ∃ t ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀,
    Subset (α := Set ((β × δ) × β × δ))
      ((fun (p : (β × δ) × β × δ) ↦
          (((e : (a : β) → α) p.1.1, (f : (a : δ) → γ) p.1.2), (e : (a : β) → α) p.2.1, (f : (a : δ) → γ) p.2.2)) ⁻¹'
        t)
      ((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')
have right : (U' ×ˢ V') ×ˢ U' ×ˢ V' ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
  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: exists (U' ×ˢ V') ×ˢ U' ×ˢ V'
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (goal)
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') ×ˢ U' ×ˢ V' ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
    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')
have right : (∃ 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: rw [mem_prod_same_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Basic (hypothesis)
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
⊢ (∃ 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')
have this : U' ×ˢ V' ∈ 𝓝 x₀ ×ˢ 𝓝 y₀
Tactic: have := prod_mem_prod U'_nhds V'_nhds
-- 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 : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ CompleteSpace.{u} (G ⧸ N)
have this₁ : IsCountablyGenerated.{u} (α := (G ⧸ N) × G ⧸ N) (𝓤 (G ⧸ N))
Tactic: haveI : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _
-- 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))
⊢ CompleteSpace.{u} (G ⧸ N)
have obtain : ∀ (u : ℕ → Set G) (hu : HasAntitoneBasis (𝓝 1) u) (u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n),
  CompleteSpace.{u} (G ⧸ N)
Tactic: obtain ⟨u, hu, u_mul⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one G
-- 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
⊢ CompleteSpace.{u} (G ⧸ N)
have hv : 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)
-- 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
⊢ CompleteSpace.{u} (G ⧸ N)
have v_anti : Antitone.{0, u} (β := Set (G ⧸ N)) fun (x : ℕ) ↦ mk '' u x
Tactic: obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)