exact this.of_eq <| by
  intro i; 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
⊢ Arith₁ fun v => if 0 < f v then g v else h v
no goals