-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem extend_Z_bilin : Continuous (extend (de.prodMap df) (fun p : β × δ => φ p.1 p.2))

Proof state:
case mk.right.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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ 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'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhd : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ (∃ t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀, t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p => ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => (φ p.2.1) p.2.2 - (φ p.1.1) p.1.2) ⁻¹' W'

Tactic:
constructor

Result:
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : 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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ 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'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhd : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ ∃ t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀, t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V'

case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : 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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ 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'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhd : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ (fun p => ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
    (fun p => (φ p.2.1) p.2.2 - (φ p.1.1) p.1.2) ⁻¹' W'

Proof state:
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : 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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ 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'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhd : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
this : U' ×ˢ V' ∈ 𝓝 x₀ ×ˢ 𝓝 y₀
⊢ ∃ t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀, t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V'

Tactic:
tauto

Result:
no goals

Proof state:
case mk.left.hf.hm
α : 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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
⊢ ∀ t ∈ 𝓝 (x₀, y₀), ∃ a, Prod.map (⇑e) (⇑f) a ∈ t

Tactic:
intro U h

Result:
case mk.left.hf.hm
α : 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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
⊢ ∃ a, Prod.map (⇑e) (⇑f) a ∈ U

Proof state:
case mk.right.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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
U_nhd : ∃ t ∈ 𝓝 x₀, ⇑e ⁻¹' t ⊆ U
V : Set δ
V_nhd : V ∈ comap (⇑f) (𝓝 y₀)
h : ∀ 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'
⊢ W' ∈
    map (fun p => (fun p => (φ p.1) p.2) p.2 - (fun p => (φ p.1) p.2) p.1)
      (comap (fun p => ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))

Tactic:
rcases U_nhd with ⟨U', U'_nhd, U'_sub⟩

Result:
case mk.right.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
inst✝² : UniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhd : V ∈ comap (⇑f) (𝓝 y₀)
h : ∀ 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'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p => (fun p => (φ p.1) p.2) p.2 - (fun p => (φ p.1) p.2) p.1)
      (comap (fun p => ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))