ENNReal weights: derive 0 < factors < ∞ a.e. from two-sided comparability

When a weight 0 < w < ∞ is comparable a.e. to a product F = a * b^(-r) with r > 0 (for example a = (M f)^δ0, b = (M g)^δ1), every factor is in (0, ∞) a.e. even though a and b can be 0 or ∞ on null sets. Get F ≠ 0 from w ≤ K F, and F ≠ ∞ from F ≤ K w. Then left_ne_zero_of_mul and right_ne_zero_of_mul give a ≠ 0 and b^(-r) ≠ 0, hence b ≠ ∞ by ENNReal.top_rpow_of_neg; ENNReal.top_mul and mul_top give a ≠ ∞ and b^(-r) ≠ ∞, hence b ≠ 0 by zero_rpow_of_neg. After that, redefine each factor to be 1 where it is 0 or ∞ (the A_1 condition survives in its a.e. form) and apply lemmas that need everywhere positivity and finiteness. A small trap: simpa [h0] using hx.2 fails when h0 is stated through set abbreviations and hx is not; use hx.2.trans_eq ((congrArg (K * ·) h0).trans (mul_zero K)), which unifies up to defeq.