α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
⊢ ∀ (b : α × γ), Cauchy (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 b)))
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
⊢ Continuous (extend (_ : DenseInducing fun p => (↑e p.fst, ↑f p.snd)) fun p => ↑(↑φ p.fst) p.snd)
refine' continuous_extend_of_cauchy _ _
case mk
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ Cauchy (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))))
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
⊢ ∀ (b : α × γ), Cauchy (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 b)))
rintro ⟨x₀, y₀⟩
case mk.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ NeBot (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))))

case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ≤
    𝓤 G
case mk
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ Cauchy (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))))
constructor
case mk.left.hf
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ NeBot (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀)))
case mk.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ NeBot (map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))))
apply NeBot.map
case mk.left.hf.hm
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ ∀ (t : Set (α × γ)), t ∈ 𝓝 (x₀, y₀) → ∃ a, (↑e a.fst, ↑f a.snd) ∈ t
case mk.left.hf
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ NeBot (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀)))
apply comap_neBot
case mk.left.hf.hm
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
⊢ ∃ a, (↑e a.fst, ↑f a.snd) ∈ U
case mk.left.hf.hm
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ ∀ (t : Set (α × γ)), t ∈ 𝓝 (x₀, y₀) → ∃ a, (↑e a.fst, ↑f a.snd) ∈ t
intro U h
case mk.left.hf.hm.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : (fun p => (↑e p.fst, ↑f p.snd)) z = x
⊢ ∃ a, (↑e a.fst, ↑f a.snd) ∈ U
case mk.left.hf.hm
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
⊢ ∃ a, (↑e a.fst, ↑f a.snd) ∈ U
rcases mem_closure_iff_nhds.1 ((de.prod df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩
case mk.left.hf.hm.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : (fun p => (↑e p.fst, ↑f p.snd)) z = x
⊢ (↑e z.fst, ↑f z.snd) ∈ U
case mk.left.hf.hm.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : (fun p => (↑e p.fst, ↑f p.snd)) z = x
⊢ ∃ a, (↑e a.fst, ↑f a.snd) ∈ U
exists z
no goals
case mk.left.hf.hm.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
U : Set (α × γ)
h : U ∈ 𝓝 (x₀, y₀)
x : α × γ
x_in : x ∈ U
z : β × δ
z_x : (fun p => (↑e p.fst, ↑f p.snd)) z = x
⊢ (↑e z.fst, ↑f z.snd) ∈ U
aesop
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ≤
    𝓤 G
suffices 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₀))) ≤ 𝓝 0 by
  rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
    prod_comap_comap_eq]
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
⊢ map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
intro W' W'_nhd
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
key :
  ∃ U,
    U ∈ comap (↑e) (𝓝 x₀) ∧
      ∃ V,
        V ∈ comap (↑f) (𝓝 y₀) ∧
          ∀ (x : β),
            x ∈ U →
              ∀ (x' : β),
                x' ∈ U →
                  ∀ (y : δ),
                    y ∈ V →
                      ∀ (y' : δ),
                        y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
have key := extend_Z_bilin_key de df hφ W'_nhd x₀ y₀
case mk.right.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
U_nhd : U ∈ comap (↑e) (𝓝 x₀)
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
key :
  ∃ U,
    U ∈ comap (↑e) (𝓝 x₀) ∧
      ∃ V,
        V ∈ comap (↑f) (𝓝 y₀) ∧
          ∀ (x : β),
            x ∈ U →
              ∀ (x' : β),
                x' ∈ U →
                  ∀ (y : δ),
                    y ∈ V →
                      ∀ (y' : δ),
                        y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rcases key with ⟨U, U_nhd, V, V_nhd, h⟩
case mk.right.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
U_nhd : ∃ t, t ∈ 𝓝 x₀ ∧ ↑e ⁻¹' t ⊆ U
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
U_nhd : U ∈ comap (↑e) (𝓝 x₀)
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rw [mem_comap] at U_nhd
case mk.right.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ↑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
U_nhd : ∃ t, t ∈ 𝓝 x₀ ∧ ↑e ⁻¹' t ⊆ U
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rcases U_nhd with ⟨U', U'_nhd, U'_sub⟩
case mk.right.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhd : ∃ t, t ∈ 𝓝 y₀ ∧ ↑f ⁻¹' t ⊆ V
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ↑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhd : V ∈ comap (↑f) (𝓝 y₀)
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ↑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rw [mem_comap] at V_nhd
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
case mk.right.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhd : ∃ t, t ∈ 𝓝 y₀ ∧ ↑f ⁻¹' t ⊆ V
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (x, y) ∈ W'
U' : Set α
U'_nhd : U' ∈ 𝓝 x₀
U'_sub : ↑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rcases V_nhd with ⟨V', V'_nhd, V'_sub⟩
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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,
    t ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
      (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' t ⊆
        (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
⊢ W' ∈
    map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))
rw [mem_map, mem_comap, nhds_prod_eq]
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
⊢ (U' ×ˢ V') ×ˢ U' ×ˢ V' ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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,
    t ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
      (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' t ⊆
        (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
exists (U' ×ˢ V') ×ˢ U' ×ˢ V'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
⊢ (U' ×ˢ V') ×ˢ U' ×ˢ V' ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
rw [mem_prod_same_iff]
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst) ⁻¹' W'
simp only [exists_prop]
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, 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_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
    (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V') ∧
    (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
      (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
constructor
no goals
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W' : Set G
W'_nhd : W' ∈ 𝓝 0
x₀ : α
y₀ : γ
this :
  map (fun p => (fun p => ↑(↑φ p.fst) p.snd) p.snd - (fun p => ↑(↑φ p.fst) p.snd) p.fst)
      (comap (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
⊢ map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p => ↑(↑φ p.fst) p.snd) (comap (fun p => (↑e p.fst, ↑f p.snd)) (𝓝 (x₀, y₀))) ≤
    𝓤 G
rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
  prod_comap_comap_eq]
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V'
have := prod_mem_prod U'_nhd V'_nhd
no goals
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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, t ∈ 𝓝 x₀ ×ˢ 𝓝 y₀ ∧ t ×ˢ t ⊆ (U' ×ˢ V') ×ˢ U' ×ˢ V'
tauto
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
p : (β × δ) × β × δ
h' : p ∈ (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V'
⊢ p ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V' ⊆
    (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
intro p h'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
p : (β × δ) × β × δ
h' : (↑e p.fst.fst ∈ U' ∧ ↑f p.fst.snd ∈ V') ∧ ↑e p.snd.fst ∈ U' ∧ ↑f p.snd.snd ∈ V'
⊢ p ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
p : (β × δ) × β × δ
h' : p ∈ (fun p => ((↑e p.fst.fst, ↑f p.fst.snd), ↑e p.snd.fst, ↑f p.snd.snd)) ⁻¹' (U' ×ˢ V') ×ˢ U' ×ˢ V'
⊢ p ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
simp only [Set.mem_preimage, Set.prod_mk_mem_set_prod_eq] at h'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right.mk.mk.mk
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
x : β
y : δ
x' : β
y' : δ
h' :
  (↑e ((x, y), x', y').fst.fst ∈ U' ∧ ↑f ((x, y), x', y').fst.snd ∈ V') ∧
    ↑e ((x, y), x', y').snd.fst ∈ U' ∧ ↑f ((x, y), x', y').snd.snd ∈ V'
⊢ ((x, y), x', y') ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
p : (β × δ) × β × δ
h' : (↑e p.fst.fst ∈ U' ∧ ↑f p.fst.snd ∈ V') ∧ ↑e p.snd.fst ∈ U' ∧ ↑f p.snd.snd ∈ V'
⊢ p ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
rcases p with ⟨⟨x, y⟩, ⟨x', y'⟩⟩
no goals
case mk.right.intro.intro.intro.intro.intro.intro.intro.intro.right.mk.mk.mk
α : Type u_1
β : Type u_4
γ : Type u_2
δ : Type u_5
G : Type u_3
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : TopologicalAddGroup α
inst✝¹³ : TopologicalSpace β
inst✝¹² : AddCommGroup β
inst✝¹¹ : TopologicalAddGroup β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : AddCommGroup γ
inst✝⁸ : TopologicalAddGroup γ
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : AddCommGroup δ
inst✝⁵ : TopologicalAddGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
inst✝² : UniformAddGroup G
inst✝¹ : SeparatedSpace G
inst✝ : CompleteSpace G
e : β →+ α
de : DenseInducing ↑e
f : δ →+ γ
df : DenseInducing ↑f
φ : β →+ δ →+ G
hφ : Continuous fun p => ↑(↑φ p.fst) p.snd
W'✝ : Set G
W'_nhd✝ : W'✝ ∈ 𝓝 0
x₀ : α
y₀ : γ
W' : Set G
W'_nhd : W' ∈ 𝓝 0
U : Set β
V : Set δ
h :
  ∀ (x : β),
    x ∈ U →
      ∀ (x' : β),
        x' ∈ U →
          ∀ (y : δ),
            y ∈ V →
              ∀ (y' : δ), y' ∈ V → (fun p => ↑(↑φ p.fst) p.snd) (x', y') - (fun p => ↑(↑φ p.fst) p.snd) (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
x : β
y : δ
x' : β
y' : δ
h' :
  (↑e ((x, y), x', y').fst.fst ∈ U' ∧ ↑f ((x, y), x', y').fst.snd ∈ V') ∧
    ↑e ((x, y), x', y').snd.fst ∈ U' ∧ ↑f ((x, y), x', y').snd.snd ∈ V'
⊢ ((x, y), x', y') ∈ (fun p => ↑(↑φ p.snd.fst) p.snd.snd - ↑(↑φ p.fst.fst) p.fst.snd) ⁻¹' W'
apply h <;> tauto