. intro h
  have hp : 1 ≤ p := one_le_of_conjugate h
  refine And.intro hp ?_
  rw [← h]
  rw [ENNReal.add_sub_cancel_left]
  rw [← lt_top_iff_ne_top]
  simp
  exact lt_of_lt_of_le zero_lt_one hp
case refine_2
p q : ℝ≥0∞
⊢ p⁻¹ + q⁻¹ = 1 → 1 ≤ p ∧ q⁻¹ = 1 - p⁻¹
no goals