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
⊢ Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace]
    (⋯.extend fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
have refine : ∀ (b : α × γ),
  Cauchy.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 b)))
Tactic: refine continuous_extend_of_cauchy _ ?_
-- 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₀ : γ
⊢ Cauchy.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
have left : NeBot.{u_5} (α := G)
  (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
    (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
Tactic: constructor
-- 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₀ : γ
left :
  NeBot.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
⊢ Cauchy.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
have right : SProd.sprod (α := Filter G) (β := Filter G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
  𝓤 G
Tactic: constructor
-- 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₀ : γ
⊢ NeBot.{u_5} (α := G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
have left : NeBot (α := β × δ) (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))
Tactic: apply NeBot.map
-- 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₀ : γ
⊢ NeBot (α := β × δ) (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))
have left : ∀ t ∈ 𝓝 (x₀, y₀), ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ t
Tactic: apply comap_neBot
-- 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₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
⊢ ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U
have left : ∀ (x : α × γ) (x_in : x ∈ U) (z : β × δ) (z_x : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z = x),
  ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U
Tactic: rcases mem_closure_iff_nhds.1 ((de.prodMap df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩
-- 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₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z = x
⊢ ∃ (a : β × δ), Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) a ∈ U
have left : Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ) z ∈ U
Tactic: exists z
-- 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₀ : γ
this :
  LE.le.{u_5} (α := 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₀))))
    (𝓝 0)
⊢ SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    𝓤 G
have rwa : SProd.sprod (α := Filter G) (β := Filter G)
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
    (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
  comap (β := G) (fun (x : G × G) ↦ x.2 - x.1) (𝓝 0)
Tactic: rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_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₀ : γ
this :
  LE.le.{u_5} (α := 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₀))))
    (𝓝 0)
rwa :
  SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    comap (β := G) (fun (x : G × G) ↦ x.2 - x.1) (𝓝 0)
⊢ SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    𝓤 G
have rwa₁ : LE.le.{u_5} (α := Filter (G × G))
  (map
    (fun (p : (β × δ) × β × δ) ↦
      ((((φ : (a : β) → δ →+ G) p.1.1 : δ →+ G) : (a : δ) → G) p.1.2,
        (((φ : (a : β) → δ →+ G) p.2.1 : δ →+ G) : (a : δ) → G) p.2.2))
    (SProd.sprod (α := Filter (β × δ)) (β := Filter (β × δ))
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))
      (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))))
  (comap (β := G) (fun (x : G × G) ↦ x.2 - x.1) (𝓝 0))
Tactic: rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_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₀ : γ
⊢ SProd.sprod (α := Filter G) (β := Filter G)
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀))))
      (map (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2)
        (comap (Prod.map (⇑e : (a : β) → α) (⇑f : (a : δ) → γ)) (𝓝 (x₀, y₀)))) ≤
    𝓤 G
have right : LE.le.{u_5} (α := 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₀))))
  (𝓝 0)
Tactic: suffices map (fun p : (β × δ) × β × δ => (fun p : β × δ => φ p.1 p.2) p.2 -
      (fun p : β × δ => φ p.1 p.2) p.1)
        (comap (fun p : (β × δ) × β × δ => ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤ 𝓝 0 by
      rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_eq]
-- 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'
⊢ 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 key : ∃ (U : Set β),
  Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U ∧
    ∃ (V : Set δ),
      Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V ∧
        ∀ 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'
Tactic: have key := extend_Z_bilin_key de df hφ W'_nhds x₀ y₀
-- 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'
key :
  ∃ (U : Set β),
    Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U ∧
      ∃ (V : Set δ),
        Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V ∧
          ∀ 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 : 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'
Tactic: rcases key with ⟨U, U_nhds, V, V_nhds, h⟩
Cleared hypotheses: key