𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure (s ×ˢ t)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : UniqueDiffWithinAt 𝕜 s x
ht : UniqueDiffWithinAt 𝕜 t y
⊢ UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
rw [uniqueDiffWithinAt_iff] at hs ht⊢
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure s ×ˢ closure t
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure (s ×ˢ t)
rw [closure_prod_eq]
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure s ×ˢ closure t
refine' ⟨_, hs.2, ht.2⟩
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
this :
  Submodule.span 𝕜 (↑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ∪ ↑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y) ≤
    Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
have : _ ≤ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)) := Submodule.span_mono
  (union_subset (subset_tangentCone_prod_left ht.2) (subset_tangentCone_prod_right hs.2))
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
this :
  ∀ ⦃x_1 : E × F⦄,
    x_1 ∈ Submodule.prod (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) (Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) →
      x_1 ∈ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
this :
  Submodule.span 𝕜 (↑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ∪ ↑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y) ≤
    Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
rw [LinearMap.span_inl_union_inr, SetLike.le_def] at this
no goals
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_1
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.128591
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y✝ : E
s t✝ : Set E
t : Set F
y : F
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s
ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t
this :
  ∀ ⦃x_1 : E × F⦄,
    x_1 ∈ Submodule.prod (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) (Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) →
      x_1 ∈ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
exact (hs.1.prod ht.1).mono this