Theorem: Vec.sum_exp_pos (CvxLean/Lib/Math/LogSumExp.lean)

State before:
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ 0 < sum (exp x)
Tactic:
apply Finset.sum_pos
State after:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i

case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty

State before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i

case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
{ intros i _; simp [Vec.exp, Real.exp_pos] }
State after:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty

State before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
{ existsi ⟨0, hn⟩; simp }
State after:
no goals

State before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ∀ i ∈ Finset.univ, 0 < exp x i
Tactic:
intros i _
State after:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ 0 < exp x i

State before:
case h
n : ℕ
hn : 0 < n
x : Fin n → ℝ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ 0 < exp x i
Tactic:
simp [Vec.exp, Real.exp_pos]
State after:
no goals

State before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ Finset.univ.Nonempty
Tactic:
existsi ⟨0, hn⟩
State after:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ⟨0, hn⟩ ∈ Finset.univ

State before:
case hs
n : ℕ
hn : 0 < n
x : Fin n → ℝ
⊢ ⟨0, hn⟩ ∈ Finset.univ
Tactic:
simp
State after:
no goals