-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) :
    LinearMap.inl 𝕜 E F '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
n : ℕ
⊢ ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n

Tactic:
rcases mem_closure_iff_nhds.1 ht _
    (eventually_nhds_norm_smul_sub_lt (c n) y (pow_pos one_half_pos n)) with
  ⟨z, hz, hzt⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
n : ℕ
z : F
hz : z ∈ {x | (fun y_1 => ‖c n • (y_1 - y)‖ < (1 / 2) ^ n) x}
hzt : z ∈ t
⊢ ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ Tendsto (HPow.hPow (1 / 2)) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ (LinearMap.inl 𝕜 E F) v ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
refine ⟨c, fun n => (d n, d' n), ?_, hc, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, (x, y) + (fun n => (d n, d' n)) n ∈ s ×ˢ t

case intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ Tendsto (fun n => c n • (fun n => (d n, d' n)) n) atTop (𝓝 ((LinearMap.inl 𝕜 E F) v))

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
n : ℕ
hn : x + d n ∈ s
⊢ (x, y) + (d n, d' n) ∈ s ×ˢ t

Tactic:
simp [hn, (hd' n).1]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
this : ∀ (n : ℕ), ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n
⊢ (LinearMap.inl 𝕜 E F) v ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
choose d' hd' using this

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ (LinearMap.inl 𝕜 E F) v ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
⊢ ∀ (n : ℕ), ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n

Tactic:
intro n

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
n : ℕ
⊢ ∃ d', y + d' ∈ t ∧ ‖c n • d'‖ < (1 / 2) ^ n

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, (x, y) + (fun n => (d n, d' n)) n ∈ s ×ˢ t

Tactic:
show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t

Result:
case intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
ht : y ∈ closure t
v : E
c : ℕ → 𝕜
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 v)
d' : ℕ → F
hd' : ∀ (n : ℕ), y + d' n ∈ t ∧ ‖c n • d' n‖ < (1 / 2) ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t