Theorem: h2 (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
⊢ Real.IsConjExponent 2 2
Tactic:
rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
State after:
no goals