-- 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
h_le :
  ∀ (n : ι),
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| ≤
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|
h_tendsto :
  Tendsto
    (fun (n : ι) ↦
      (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 ((↑L : ℝ) * ε / 2))
h_lt : (↑L : ℝ) * ε / 2 < (↑L : ℝ) * ε
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι)
            {x : ι |
              (fun (a : ι) ↦
                  (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y a ω - X a ω‖} +
                      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X a) μ'') fun (ω : E) ↦ F ω)
                          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
                    (↑L : ℝ) * ε)
                x}
            x →
          Membership.mem (γ := Set ι)
            {x : ι |
              (fun (n : ι) ↦
                  |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
                        (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
                    (↑L : ℝ) * ε)
                x}
            x}
      a
⊢ ∀ᶠ (n : ι) in l,
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
      (↑L : ℝ) * ε
have h₁ : ∀ (a : ι),
  (↑L : ℝ) * (ε / 2) + M * μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y a ω - X a ω‖} +
        |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X a) μ'') fun (ω : E) ↦ F ω)
            (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
      (↑L : ℝ) * ε →
    |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y a) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
      (↑L : ℝ) * ε
Tactic: filter_upwards [h_tendsto.eventually_lt_const h_lt] with n hn using (h_le n).trans_lt hn