-- 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:
α : 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)
this :
  map (fun t => t.2 - t.1) (comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) ×ˢ
      map (fun t => t.2 - t.1) (comap (fun p => (f p.1, f p.2)) (𝓝 (y₀, y₀))) ≤
    𝓝 0 ×ˢ 𝓝 0
⊢ 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)

Tactic:
rwa [prod_map_map_eq] at this

Result:
no goals

Proof state:
case intro.intro.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 : Set (β × β)
U_in : U ∈ comap ee (𝓝 (x₀, x₀))
V : Set (δ × δ)
V_in : V ∈ comap ff (𝓝 (y₀, y₀))
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p => (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
⊢ ∃ 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

Tactic:
rw [nhds_prod_eq, ← prod_comap_comap_eq, mem_prod_same_iff] at U_in V_in

Result:
case intro.intro.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 : Set (β × β)
U_in : ∃ t ∈ comap (⇑e) (𝓝 x₀), t ×ˢ t ⊆ U
V : Set (δ × δ)
V_in : ∃ t ∈ comap (⇑f) (𝓝 y₀), t ×ˢ t ⊆ V
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p => (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
⊢ ∃ 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

Proof state:
case intro.intro.intro.intro.intro.intro.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 : Set (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p => (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
U₁ : Set β
U₁_in : U₁ ∈ comap (⇑e) (𝓝 x₀)
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : V₁ ∈ comap (⇑f) (𝓝 y₀)
HV₁ : V₁ ×ˢ V₁ ⊆ V
⊢ ∃ 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

Tactic:
exists U₁, U₁_in, V₁, V₁_in

Result:
case intro.intro.intro.intro.intro.intro.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 : Set (β × β)
V : Set (δ × δ)
H :
  ∀ (x : β × β) (y : δ × δ),
    x ∈ U → y ∈ V → (fun p => (φ p.1) p.2) ((x, y).1.2 - (x, y).1.1, (x, y).2.2 - (x, y).2.1) ∈ W
U₁ : Set β
U₁_in : U₁ ∈ comap (⇑e) (𝓝 x₀)
HU₁ : U₁ ×ˢ U₁ ⊆ U
V₁ : Set δ
V₁_in : V₁ ∈ comap (⇑f) (𝓝 y₀)
HV₁ : V₁ ×ˢ V₁ ⊆ V
⊢ ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p => (φ p.1) p.2) (x' - x, y' - y) ∈ W