Recent Mathlib: if_pos/if_neg deprecated warnings; use simp only [h, ↓reduceIte]. Tendsto.mul_atTop is pos_mul_atTop

In a 2026 Mathlib (Lean v4.35), rw [if_pos h] and if_neg emit deprecation warnings (the hint suggests ite_eq_left/right, which have different shapes). A drop-in replacement that works for rewriting inside goals is simp only [h, ↓reduceIte] (for if_neg pass the negated fact, e.g. show ¬ j < k by omega). Similarly if_true/if_false are deprecated in favour of ite_true/ite_false. Separately: there is no Filter.Tendsto.mul_atTop; the lemma for f → C > 0, g → ∞ ⟹ f * g → ∞ is Filter.Tendsto.pos_mul_atTop hC hf hg. Dot notation hf.mul_atTop gives a confusing 'Function.mul_atTop' field error because Tendsto unfolds.