-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
hn :
  ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
succ :
  ∀
    (hn :
      ∀
        (h_subG :
          ∀ i < HSub.hSub (α := ℕ) 0 1,
            HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ)
    (h_subG :
      ∀ i < HAdd.hAdd (α := ℕ) 0 1 - 1,
        HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), Y i ω)
      (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), cY i) μ
succ₁ :
  ∀ (n : ℕ),
    (∀
        (hn :
          ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
            HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
        (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ) →
      ∀
        (hn :
          ∀
            (h_subG :
              ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
            HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ)
        (h_subG :
          ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ

Tactic:
induction n with
    | zero => simp [h0]
    | succ n =>
      specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia

Premises used: MeasureTheory.StronglyMeasurable.measurable, Finset.mem_range, Finset.range, HAdd.hAdd, MeasureTheory.StronglyMeasurable.mono, ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGF, Finset.measurable_fun_sum, MeasureTheory.Filtration.mono, MeasureTheory.Filtration.le, ProbabilityTheory.HasSubgaussianMGF.zero, OfNat.ofNat, Finset.sum_range_succ