Theorem: ENNReal.one_le_of_conjugate' (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ q
Tactic:
rw [add_comm] at hpq
State after:
p q : ℝ≥0∞
hpq : q⁻¹ + p⁻¹ = 1
⊢ 1 ≤ q

State before:
p q : ℝ≥0∞
hpq : q⁻¹ + p⁻¹ = 1
⊢ 1 ≤ q
Tactic:
exact one_le_of_conjugate hpq
State after:
no goals