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
case inl.intro.some
q : ℝ≥0∞
hq✝ : q ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hq' : q ≠ 0
p : ℝ≥0
hpq : (some p)⁻¹ + q⁻¹ = 1
hp✝ : some p ≠ ⊤
hp : 1 < some p ∧ some p ≠ ⊤
hp' : some p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal (some p)) ↑(ENNReal.toNNReal q)
no goals