cases eq_or_lt_of_le (le_top : q ≤ ⊤) with
| inl hq =>
  simp [hq] at h ⊢
  simpa [inv_eq_iff_eq_inv] using h
| inr hq =>
  refine Or.inl ?_
  simp [← lt_top_iff_ne_top, hp, hq]
  simp_rw [← ENNReal.inv_lt_one]
  rw [← h]
  rw [lt_top_iff_ne_top] at hp hq
  refine And.intro ?_ ?_
  . refine ENNReal.lt_add_right ?_ ?_
    . rw [← lt_top_iff_ne_top]
      simp
      exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate h)
    . rwa [ENNReal.inv_ne_zero]
  . rw [add_comm]
    refine ENNReal.lt_add_right ?_ ?_
    . rw [← lt_top_iff_ne_top]
      simp
      exact lt_of_lt_of_le zero_lt_one (one_le_of_conjugate' h)
    . rwa [ENNReal.inv_ne_zero]
case inr
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
hp : p < ⊤
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
no goals