-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem extend_Z_bilin_key (x₀ : α) (y₀ : γ) : ∃ U ∈ comap e (𝓝 x₀), ∃ V ∈ comap f (𝓝 y₀),
    ∀ x ∈ U, ∀ x' ∈ U, ∀ (y) (_ : y ∈ V) (y') (_ : y' ∈ V),
    (fun p : β × δ => φ p.1 p.2) (x', y') - (fun p : β × δ => φ p.1 p.2) (x, y) ∈ W'

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p => (fun p => (φ p.1) p.2) (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_nhd : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'

Tactic:
have :
  ∃ U₁ ∈ comap e (𝓝 x₀), ∃ V₁ ∈ comap f (𝓝 y₀), ∀ (x) (_ : x ∈ U₁) (x') (_ : x' ∈ U₁),
    ∀ (y) (_ : y ∈ V₁) (y') (_ : y' ∈ V₁), (fun p : β × δ => φ p.1 p.2) (x' - x, y' - y) ∈ W := by
  rcases tendsto_prod_iff.1 lim_φ_sub_sub W W_nhd with ⟨U, U_in, V, V_in, H⟩
  rw [nhds_prod_eq, ← prod_comap_comap_eq, mem_prod_same_iff] at U_in V_in
  rcases U_in with ⟨U₁, U₁_in, HU₁⟩
  rcases V_in with ⟨V₁, V₁_in, HV₁⟩
  exists U₁, U₁_in, V₁, V₁_in
  intro x x_in x' x'_in y y_in y' y'_in
  exact H _ _ (HU₁ (mk_mem_prod x_in x'_in)) (HV₁ (mk_mem_prod y_in y'_in))

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p => (fun p => (φ p.1) p.2) (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_nhd : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
this :
  ∃ U₁ ∈ comap (⇑e) (𝓝 x₀),
    ∃ V₁ ∈ comap (⇑f) (𝓝 y₀), ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
have lim_sub_sub :
  Tendsto (fun p : (β × β) × δ × δ => (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0) := by
  have := Filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀)
  rwa [prod_map_map_eq] at this

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (fun p => (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0)
⊢ Tendsto (fun p => (fun p => (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'

Tactic:
have lim_φ : Filter.Tendsto (fun p : β × δ => φ p.1 p.2) (𝓝 (0, 0)) (𝓝 0) := by
  simpa using hφ.tendsto (0, 0)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
inst✝ : UniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u => (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u => (f u.1, f u.2)
lim_φ : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ ∃ U ∈ comap (⇑e) (𝓝 x₀),
    ∃ V ∈ comap (⇑f) (𝓝 y₀),
      ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p => (φ p.1) p.2) (x', y') - (fun p => (φ p.1) p.2) (x, y) ∈ W'