refine Or.inl ?_
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
case inr.inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
hq : q < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤