-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α →ₛ ℝ≥0
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
const :
  ∀ (c : ℝ≥0) {s : Set α} (hs : MeasurableSet s) {L : ℝ≥0∞}
    (hL :
      L < ∫⁻ (x : α), (↑((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
    ∃ (g : α →ₛ ℝ≥0),
      (∀ (x : α),
          LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0)
            ((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
        ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
add :
  ∀ ⦃f₁ f₂ : α →ₛ ℝ≥0⦄,
    Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
        (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0)) →
      ∀
        (h₁ :
          ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
            ∃ (g : α →ₛ ℝ≥0),
              (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
                ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧
                  L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
        (h₂ :
          ∀ {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
            ∃ (g : α →ₛ ℝ≥0),
              (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
                ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧
                  L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
        {L : ℝ≥0∞} (hL : L < ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ),
        ∃ (g : α →ₛ ℝ≥0),
          (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ + f₂ : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
            ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ ∃ (g : α →ₛ ℝ≥0),
    (∀ (x : α), LE.le (α := ℝ≥0) ((g : (a : α) → ℝ≥0) x : ℝ≥0) ((f : (a : α) → ℝ≥0) x : ℝ≥0)) ∧
      ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞ ∧ L < ∫⁻ (x : α), (↑((g : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
induction f using MeasureTheory.SimpleFunc.induction generalizing L with
  | @const c s hs =>
    simp only [hs, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
      piecewise_eq_indicator, lintegral_indicator, lintegral_const, Measure.restrict_apply',
      ENNReal.coe_indicator, Function.const_apply] at hL
    have c_ne_zero : c ≠ 0 := by
      intro hc
      simp only [hc, ENNReal.coe_zero, zero_mul, not_lt_zero] at hL
    have : L / c < μ s := by
      rwa [ENNReal.div_lt_iff, mul_comm]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]
    obtain ⟨t, ht, ts, mlt, t_top⟩ :
      ∃ t : Set α, MeasurableSet t ∧ t ⊆ s ∧ L / ↑c < μ t ∧ μ t < ∞ :=
      Measure.exists_subset_measure_lt_top hs this
    refine ⟨piecewise t ht (const α c) (const α 0), fun x => ?_, ?_, ?_⟩
    · refine indicator_le_indicator_of_subset ts (fun x => ?_) x
      exact zero_le
    · simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero, univ_inter,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', ENNReal.mul_lt_top ENNReal.coe_lt_top t_top]
    · simp only [ht, const_zero, coe_piecewise, coe_const, SimpleFunc.coe_zero,
        piecewise_eq_indicator, ENNReal.coe_indicator, Function.const_apply, lintegral_indicator,
        lintegral_const, Measure.restrict_apply', univ_inter]
      rwa [mul_comm, ← ENNReal.div_lt_iff]
      · simp only [c_ne_zero, Ne, ENNReal.coe_eq_zero, not_false_iff, true_or]
      · simp only [Ne, coe_ne_top, not_false_iff, true_or]
  | @add f₁ f₂ _ h₁ h₂ =>
    replace hL : L < ∫⁻ x, f₁ x ∂μ + ∫⁻ x, f₂ x ∂μ := by
      rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
    by_cases hf₁ : ∫⁻ x, f₁ x ∂μ = 0
    · simp only [hf₁, zero_add] at hL
      rcases h₂ hL with ⟨g, g_le, g_top, gL⟩
      refine ⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩
      simp only [SimpleFunc.coe_add, Pi.add_apply, le_add_iff_nonneg_left, zero_le']
    by_cases hf₂ : ∫⁻ x, f₂ x ∂μ = 0
    · simp only [hf₂, add_zero] at hL
      rcases h₁ hL with ⟨g, g_le, g_top, gL⟩
      refine ⟨g, fun x => (g_le x).trans ?_, g_top, gL⟩
      simp only [SimpleFunc.coe_add, Pi.add_apply, le_add_iff_nonneg_right, zero_le']
    obtain ⟨L₁, hL₁, L₂, hL₂, hL⟩ : ∃ L₁ < ∫⁻ x, f₁ x ∂μ, ∃ L₂ < ∫⁻ x, f₂ x ∂μ, L < L₁ + L₂ :=
      ENNReal.exists_lt_add_of_lt_add hL hf₁ hf₂
    rcases h₁ hL₁ with ⟨g₁, g₁_le, g₁_top, hg₁⟩
    rcases h₂ hL₂ with ⟨g₂, g₂_le, g₂_top, hg₂⟩
    refine ⟨g₁ + g₂, fun x => add_le_add (g₁_le x) (g₂_le x), ?_, ?_⟩
    · apply lt_of_le_of_lt _ (add_lt_top.2 ⟨g₁_top, g₂_top⟩)
      rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
      exact le_rfl
    · apply hL.trans ((ENNReal.add_lt_add hg₁ hg₂).trans_le _)
      rw [← lintegral_add_left g₁.measurable.coe_nnreal_ennreal]
      simp only [coe_add, Pi.add_apply, ENNReal.coe_add, le_rfl]

Premises used: Function.const_apply, zero_le, MeasureTheory.lintegral_const, le_add_iff_nonneg_right, MeasureTheory.SimpleFunc.const, le_rfl, MeasureTheory.SimpleFunc.coe_add, true_or, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Ne, ENNReal.coe_eq_zero, ENNReal.coe_add, Set.univ_inter, zero_add, Pi.add_apply, MeasureTheory.lintegral_indicator, mul_comm, zero_le', MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, add_zero, not_false_iff, MeasureTheory.Measure.restrict_apply', ENNReal.div_lt_iff, MeasureTheory.SimpleFunc.coe_const, le_add_iff_nonneg_left, ENNReal.coe_indicator, ENNReal.coe_ne_top, Set