rw [lt_top_iff_ne_top] at hp hq
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ < p⁻¹ + q⁻¹ ∧ q⁻¹ < p⁻¹ + q⁻¹