-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_1 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_2 : SeminormedAddCommGroup E
inst_3 : SecondCountableTopology E
inst_4 : BorelSpace E
X : ι → Ω'' → E
inst_5 : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) X l Z (fun (x : ι) ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (Y n x)) μ''
h_int_X : Integrable (ε := ℝ) (fun (x : Ω'') ↦ F (X n x)) μ''
h_int_sub : Integrable (ε := ℝ) (fun (a : Ω'') ↦ ‖F (Y n a) - F (X n a)‖) μ''
calc :
  ∫ (a : Ω''), ‖F (Y n a) - F (X n a)‖ ∂μ'' =
    HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
calc₁ :
  HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'') ≤
    HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')
      (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'')
⊢ norm (E := ℝ) (∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ'') ≤
    (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
have calc₂ : HAdd.hAdd (α := ℝ) (∫ (a : Ω'') in {x : Ω'' | ‖Y n x - X n x‖ < ε / 2}, (↑L : ℝ) * (ε / 2) ∂μ'')
    (∫ (a : Ω'') in {x : Ω'' | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'') =
  (↑L : ℝ) * (ε / 2) * μ''.real {x : Ω'' | ‖Y n x - X n x‖ < ε / 2} + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}
Tactic: calc ‖∫ a, F (Y n a) - F (X n a) ∂μ''‖
    _ ≤ ∫ a, ‖F (Y n a) - F (X n a)‖ ∂μ'' := norm_integral_le_integral_norm _
    -- Either `‖Y n x - X n x‖` is smaller than `ε / 2`, or it is not
    _ = ∫ a in {x | ‖Y n x - X n x‖ < ε / 2}, ‖F (Y n a) - F (X n a)‖ ∂μ''
        + ∫ a in {x | ε / 2 ≤ ‖Y n x - X n x‖}, ‖F (Y n a) - F (X n a)‖ ∂μ'' := by
      symm
      simp_rw [← not_lt]
      refine integral_add_compl₀ ?_ h_int_sub
      exact nullMeasurableSet_lt (by fun_prop) (by fun_prop)
    -- If it is smaller, we use the Lipschitz property of `F`
    -- If not, we use the boundedness of `F`.
    _ ≤ ∫ a in {x | ‖Y n x - X n x‖ < ε / 2}, L * (ε / 2) ∂μ''
        + ∫ a in {x | ε / 2 ≤ ‖Y n x - X n x‖}, M ∂μ'' := by
      gcongr ?_ + ?_
      · refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_
        · exact nullMeasurableSet_lt (by fun_prop) (by fun_prop)
        · exact fun x hx ↦ hF_lip.norm_sub_le_of_le hx.le
      · refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_
        rw [← dist_eq_norm]
        convert!
          hF_bounded _
            _
              -- The goal is now a simple computation

    -- The goal is now a simple computation
    _ = L * (ε / 2) * μ''.real {x | ‖Y n x - X n x‖ < ε / 2}
        + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} := by
      simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter,
        smul_eq_mul]
      ring
    _ ≤ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} := by
      rw [mul_assoc]
      gcongr
      grw [measureReal_le_one, mul_one]