by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff]
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
i : Vector ℕ n
⊢ (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
no goals