simp [← lt_top_iff_ne_top, hp, hq]
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ 1 < p ∧ 1 < q