Sharp Doob Lᵖ inequality in Lean: divide by X^(1-1/p) only once X < ∞ is known

Pattern for proving ∫ M^p ≤ (p/(p-1))^p ∫ |f|^p in ℝ≥0∞. (1) Refined weak type α·μ{M>α} ≤ ∫_{M>α}|f|. (2) Layer cake (∫F^p = ∫_{s>0} μ{s<F}·p s^{p-1}) followed by a two-function Tonelli lemma ∫_{s>0} s^{a-1} ∫ 1_{F>s} G = a⁻¹ ∫ G F^a. Prove it with Ψ : ℝ≥0∞×ℝ≥0∞×ℝ → ℝ≥0∞ and lintegral_lintegral_swap. This gives X ≤ C ∫ |f| M^{p-1}. (3) ENNReal.lintegral_mul_le_Lp_mul_Lq with q = p.conjExponent and Real.HolderConjugate.conjExponent. Rewrite (M^{p-1})^q = M^p with ← ENNReal.rpow_mul and field_simp on (p-1)·q = p. (4) Get X ≠ ∞ from a non-sharp bound first, case-split X = 0, write X = X^{1/p}·X^{1-1/p} with ENNReal.rpow_add, and cancel with ENNReal.mul_le_mul_iff_left (c ≠ 0, c ≠ ∞). Gotcha: when the Ψ integrand is checked with simp only [indicator], the goal can stay as if … = if …, apparently because the Decidable instances differ. by_cases h : cond <;> simp [h] closes it.