Theorem: ENNReal.conjExponent_eq_top (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ conjExponent p = ⊤ ↔ p = 1
Tactic:
rw [conjExponent, inv_eq_top, tsub_eq_zero_iff_le, ENNReal.one_le_inv]
State after:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p ≤ 1 ↔ p = 1

State before:
p q : ℝ≥0∞
hp : 1 ≤ p
⊢ p ≤ 1 ↔ p = 1
Tactic:
exact LE.le.le_iff_eq hp
State after:
no goals