simp at *
case inl.intro.some.some
p : ℝ≥0
hp✝ : some p ≠ ⊤
hp : 1 < some p ∧ some p ≠ ⊤
hp' : some p ≠ 0
q : ℝ≥0
hq✝ : some q ≠ ⊤
hq : 1 < some q ∧ some q ≠ ⊤
hq' : some q ≠ 0
hpq : (some p)⁻¹ + (some q)⁻¹ = 1
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal (some p)) ↑(ENNReal.toNNReal (some q))
case inl.intro.some.some
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p.IsConjExponent q