-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem extend_Z_bilin_aux (x₀ : α) (y₁ : δ) : ∃ U₂ ∈ comap e (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂,
    (fun p : β × δ => φ p.1 p.2) (x' - x, y₁) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim : Tendsto ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 0)
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
rw [tendsto_prod_self_iff] at lim

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
have lim := lim2.comp lim1

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim : Tendsto ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 0)
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Tactic:
simp_rw [forall_mem_comm]

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ (a b : β), a ∈ U₂ → b ∈ U₂ → (φ (b - a)) y₁ ∈ W'

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

Tactic:
have lim1 : Tendsto (fun a : β × β => (a.2 - a.1, y₁))
    (comap e Nx ×ˢ comap e Nx) (𝓝 (0, y₁)) := by
  have := Tendsto.prod_mk (tendsto_sub_comap_self de x₀)
    (tendsto_const_nhds : Tendsto (fun _ : β × β => y₁) (comap ee <| 𝓝 (x₀, x₀)) (𝓝 y₁))
  rw [nhds_prod_eq, prod_comap_comap_eq, ← nhds_prod_eq]
  exact (this :)

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous fun p => (φ p.1) p.2
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u => (e u.1, e u.2)
lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ (a b : β), a ∈ U₂ → b ∈ U₂ → (φ (b - a)) y₁ ∈ W'

Tactic:
exact lim W' W'_nhd

Result:
no goals