cases p with
| none =>
  simpa [inv_eq_iff_eq_inv] using h
| some p =>
  cases q with
  | none =>
    simpa [inv_eq_iff_eq_inv] using h
  | some q =>
    simp
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ p ≠ ⊤ ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
no goals