-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
calc :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) x) ≤
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω) ^ (↑p : ℝ)) x)
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * Y ω) ^ (↑q : ℝ)) x)
        (1 / (↑q : ℝ))
calc₁ :
  HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω) ^ (↑p : ℝ)) x)
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * Y ω) ^ (↑q : ℝ)) x)
        (1 / (↑q : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))
⊢ mgf (m := mΩ) (fun (ω : Ω) ↦ X ω + Y ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp
      ((↑(HPow.hPow (β := ℕ)
                (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
                  ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
                2) :
            ℝ) *
          HPow.hPow (β := ℕ) t 2 /
        2)
have calc₂ : rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
    rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ)) =
  rexp
    (HPow.hPow (β := ℕ) ((↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX) : ℝ) + (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY) : ℝ)) 2 *
        HPow.hPow (β := ℕ) t 2 /
      2)
Tactic: calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg)