. rw [← lt_top_iff_ne_top]
  simp
  exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
case inr.inr.refine_1.refine_1
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p⁻¹ ≠ ⊤

case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0
case inr.inr.refine_1.refine_2
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ q⁻¹ ≠ 0