cases hpq with
| inl hpq => rcases hpq with ⟨_, hq'⟩; contradiction
| inr hpq => rcases hpq with ⟨hp', _⟩; contradiction
case inr
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hpq : p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
no goals