rcases hpq with ⟨hp, hq⟩
case inl
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
hpq : (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)