cases eq_or_lt_of_le (le_top : p ≤ ⊤) with
| inl hp =>
  simp [hp] at h ⊢
  simpa [inv_eq_iff_eq_inv] using h
| inr hp =>
  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]
p q : ℝ≥0∞
h : p⁻¹ + q⁻¹ = 1
⊢ (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤ ∨ p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
no goals