-- Mathlib/Analysis/MeanInequalities.lean
theorem young_inequality (a b : ℝ≥0∞) {p q : ℝ} (hpq : p.IsConjExponent q) :
    a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Proof state:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
refine le_trans le_top (le_of_eq ?_)

Result:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Proof state:
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ p.toNNReal ≠ 0

Tactic:
simp [hpq.pos]

Result:
no goals

Proof state:
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ q.toNNReal ≠ 0

Tactic:
simp [hpq.symm.pos]

Result:
no goals

Proof state:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
rcases h with h | h <;> rw [h] <;> simp [h, hpq.pos, hpq.symm.pos]

Result:
no goals

Proof state:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal

Tactic:
exact NNReal.young_inequality_real a.toNNReal b.toNNReal hpq

Result:
no goals

Proof state:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : ¬(a = ⊤ ∨ b = ⊤)
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
push_neg at h

Result:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Proof state:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
repeat rw [div_eq_mul_inv]

Result:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Proof state:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q

Tactic:
rw [div_eq_mul_inv]

Result:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Proof state:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
rw [← coe_toNNReal h.left, ← coe_toNNReal h.right, ← coe_mul, ← coe_rpow_of_nonneg _ hpq.nonneg,
  ← coe_rpow_of_nonneg _ hpq.symm.nonneg, ENNReal.ofReal, ENNReal.ofReal, ←
  @coe_div (Real.toNNReal p) _ (by simp [hpq.pos]), ←
  @coe_div (Real.toNNReal q) _ (by simp [hpq.symm.pos]), ← coe_add, coe_le_coe]

Result:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal

Proof state:
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
by_cases h : a = ⊤ ∨ b = ⊤

Result:
case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : a = ⊤ ∨ b = ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.IsConjExponent q
h : ¬(a = ⊤ ∨ b = ⊤)
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q