-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem mapsTo_tangentCone_pi {ι : Type*} [DecidableEq ι] {E : ι → Type*}
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] {s : ∀ i, Set (E i)} {x : ∀ i, E i}
    {i : ι} (hi : ∀ j ≠ i, x j ∈ closure (s j)) :
    MapsTo (LinearMap.single 𝕜 E i) (tangentConeAt 𝕜 (s i) (x i))
      (tangentConeAt 𝕜 (Set.pi univ s) x)

Proof state:
case intro.intro.intro.intro.refine_2.inr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ 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
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
⊢ (LinearMap.single 𝕜 E i) w ∈ tangentConeAt 𝕜 (univ.pi s) x

Tactic:
refine ⟨c, fun n => Function.update (d' n) i (d n), hd.mono fun n hn j _ => ?_, hc,
    tendsto_pi_nhds.2 fun j => ?_⟩

Result:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
n : ℕ
hn : x i + d n ∈ s i
j : ι
x✝ : j ∈ univ
⊢ (x + (fun n => Function.update (d' n) i (d n)) n) j ∈ s j

case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop
    (𝓝 ((LinearMap.single 𝕜 E i) w j))

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n

Tactic:
rcases mem_closure_iff_nhds.1 (hi j hj) _
    (eventually_nhds_norm_smul_sub_lt (c n) (x j) (pow_pos one_half_pos n)) with
  ⟨z, hz, hzs⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
j : ι
hj : j ≠ i
z : E j
hz : z ∈ {x_1 | (fun y => ‖c n • (y - x j)‖ < (1 / 2) ^ n) x_1}
hzs : z ∈ s j
⊢ ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n

Proof state:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
n : ℕ
hn : x i + d n ∈ s i
j : ι
x✝ : j ∈ univ
⊢ (x + (fun n => Function.update (d' n) i (d n)) n) j ∈ s j

Tactic:
rcases em (j = i) with (rfl | hj) <;> simp [*]

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop
    (𝓝 ((LinearMap.single 𝕜 E i) w j))

Tactic:
rcases em (j = i) with (rfl | hj)

Result:
case intro.intro.intro.intro.refine_2.inl
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
c : ℕ → 𝕜
hc : Tendsto (fun n => ‖c n‖) atTop atTop
d' : ℕ → (j : ι) → E j
j : ι
hi : ∀ (j_1 : ι), j_1 ≠ j → x j_1 ∈ closure (s j_1)
w : E j
d : ℕ → E j
hd : ∀ᶠ (n : ℕ) in atTop, x j + d n ∈ s j
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
hd's : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → x j_1 + d' n j_1 ∈ s j_1
hcd' : ∀ (n : ℕ) (j_1 : ι), j_1 ≠ j → ‖c n • d' n j_1‖ < (1 / 2) ^ n
⊢ Tendsto (fun i => (c i • (fun n => Function.update (d' n) j (d n)) i) j) atTop (𝓝 ((LinearMap.single 𝕜 E j) w j))

case intro.intro.intro.intro.refine_2.inr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : DecidableEq ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)
w : E i
c : ℕ → 𝕜
d : ℕ → E i
hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
d' : ℕ → (j : ι) → E j
hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j
hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n
j : ι
hj : ¬j = i
⊢ Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop
    (𝓝 ((LinearMap.single 𝕜 E i) w j))