Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : 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[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup 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_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
cont_flip : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ.flip p.1) p.2
U₂ : Set β
U₂_nhds : U₂ ∈ comap (⇑e) (𝓝 x₀)
HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, 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'

Tactic:
rcases extend_Z_bilin_aux df cont_flip W_nhds y₀ x₁ with ⟨V₂, V₂_nhds, HV⟩

Goal state after:
α : 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[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup 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_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
cont_flip : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ.flip p.1) p.2
U₂ : Set β
U₂_nhds : U₂ ∈ comap (⇑e) (𝓝 x₀)
HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W
V₂ : Set δ
V₂_nhds : V₂ ∈ comap (⇑f) (𝓝 y₀)
HV : ∀ x ∈ V₂, ∀ x' ∈ V₂, (fun p ↦ (φ.flip p.1) p.2) (x' - x, x₁) ∈ 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'