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

State before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ 1 ≤ p
Tactic:
rw [← ENNReal.inv_le_inv, inv_one]
State after:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ p⁻¹ ≤ 1

State before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
⊢ p⁻¹ ≤ 1
Tactic:
simp [← hpq]
State after:
no goals