cases conjugate_cases hpq with
| inr hpq =>
  simp at *
  cases hpq with
  | inl hpq => rcases hpq with ⟨_, hq'⟩; contradiction
  | inr hpq => rcases hpq with ⟨hp', _⟩; contradiction
| inl hpq =>
  rcases hpq with ⟨hp, hq⟩
  have hp' : p ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact one_le_of_conjugate hpq
  have hq' : q ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact one_le_of_conjugate' hpq
  cases p with | none => contradiction | some p =>
  cases q with | none => contradiction | some q =>
  simp at *
  constructor
  . norm_cast
  . rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
    norm_cast at hpq
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
no goals