-- 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)
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))
rwa₂ :
  LE.le.{u_5} (α := Filter G)
    (map (fun (x : G × G) ↦ x.2 - x.1)
      (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₀))))))
    (𝓝 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)
  (map
    ((fun (x : G × G) ↦ x.2 - x.1) ∘ 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₀)))))
  (𝓝 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]