-- 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
W' : Set G
W'_nhds : Membership.mem (γ := Filter G) (𝓝 0) W'
inst_12 : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : (u : β × β) → α × α := fun (u : β × β) ↦ ((e : (a : β) → α) u.1, (e : (a : β) → α) u.2)
ff : (u : δ × δ) → γ × γ := fun (u : δ × δ) ↦ ((f : (a : δ) → γ) u.1, (f : (a : δ) → γ) u.2)
lim_φ : Tendsto (β := G) (fun (p : β × δ) ↦ (((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (β := G)
    (fun (p : Prod.{u_2, u_4} (β × β) (δ × δ)) ↦
      (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G))
        (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : Membership.mem (γ := Filter G) (𝓝 0) W
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ 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₁,
          (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
cont_flip :
  Continuous[instTopologicalSpaceProd, inst_10.toTopologicalSpace] fun (p : δ × β) ↦
    (((φ.flip : (a : δ) → β →+ G) p.1 : β →+ G) : (a : β) → G) p.2
U₂ : Set β
U₂_nhds : Membership.mem (γ := Filter β) (comap (⇑e : (a : β) → α) (𝓝 x₀)) U₂
HU :
  ∀ x ∈ U₂,
    ∀ x' ∈ U₂, (fun (p : β × δ) ↦ ((((φ : (a : β) → δ →+ G) p.1 : δ →+ G) : (a : δ) → G) p.2 : G)) (x' - x, y₁) ∈ W
V₂ : Set δ
V₂_nhds : Membership.mem (γ := Filter δ) (comap (⇑f : (a : δ) → γ) (𝓝 y₀)) V₂
HV :
  ∀ x ∈ V₂,
    ∀ x' ∈ V₂,
      (fun (p : δ × β) ↦ (((((φ.flip : δ →+ β →+ G) : (a : δ) → β →+ G) p.1 : β →+ G) : (a : β) → G) p.2 : G))
          (x' - x, x₁) ∈
        W
x : β
xU₁ : x ∈ U₁
xU₂ : x ∈ U₂
x' : β
x'U₁ : x' ∈ U₁
x'U₂ : x' ∈ U₂
y : δ
yV₁ : y ∈ V₁
yV₂ : y ∈ V₂
y' : δ
y'V₁ : y' ∈ V₁
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'
have key_formula : HSub.hSub (α := G) (β := G) ((((φ : (a : β) → δ →+ G) x' : δ →+ G) : (a : δ) → G) y' : G)
    ((((φ : (a : β) → δ →+ G) x : δ →+ G) : (a : δ) → G) y : G) =
  HAdd.hAdd (β := G)
    (HAdd.hAdd (β := G)
      (HAdd.hAdd (α := G) (β := G) ((((φ : (a : β) → δ →+ G) (x' - x) : δ →+ G) : (a : δ) → G) y₁ : G)
        ((((φ : (a : β) → δ →+ G) (x' - x) : δ →+ G) : (a : δ) → G) (y' - y₁) : G))
      ((((φ : (a : β) → δ →+ G) x₁ : δ →+ G) : (a : δ) → G) (y' - y) : G))
    ((((φ : (a : β) → δ →+ G) (x - x₁) : δ →+ G) : (a : δ) → G) (y' - y) : G)
Tactic: have key_formula : φ x' y' - φ x y
    = φ (x' - x) y₁ + φ (x' - x) (y' - y₁) + φ x₁ (y' - y) + φ (x - x₁) (y' - y) := by simp; abel