awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
refine_1 : Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * (ε / 2)))
⊢ Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * ε / 2))

Tactic:
rw [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
⊢ Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * (ε / 2)))

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
⊢ Tendsto (fun (n : ι) ↦ (↑L : ℝ) * (ε / 2)) l (𝓝 ((↑L : ℝ) * (ε / 2)))

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
⊢ ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ''.real {x : Ω'' | ε ≤ ‖(Y - X) i x‖}) l (𝓝 0)

Tactic:
simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY

Premises used: MeasureTheory.tendstoInMeasure_iff_measureReal_norm, sub_zero, Pi.zero_apply
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 : ι) ↦ μ'') μ'
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 ω)|
hXY : ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ''.real {x : Ω'' | ε ≤ ‖(Y - X) i x‖}) l (𝓝 0)
⊢ 0 < ε / 2

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 : ι) ↦ μ'') μ'
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 ω)|
hXY : ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ''.real {x : Ω'' | ε ≤ ‖(Y - X) i x‖}) l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ μ''.real {ω : Ω'' | ε / 2 ≤ ‖Y n ω - X n ω‖}) l (𝓝 0)

Tactic:
exact hXY (ε / 2) (by positivity)

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
replace hXZ := hXZ.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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_1 : 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 ω)|
hXZ :
  Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))
⊢ ∀ (f : E → ℝ),
    (∃ (C : ℝ), ∀ (x y : E), dist (f x) (f y) ≤ C) →
      (∃ (L : NNReal), LipschitzWith L f) →
        Tendsto (β := ℝ)
          (fun (i : ι) ↦
            ∫ (ω : E),
              f
                ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X i) μ'') ⋯) :
                Measure E))
          l
          (𝓝
            (∫ (ω : E),
              f
                ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) :
                Measure E)))

Tactic:
simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hXZ

Premises used: MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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_1 : 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 ω)|
hXZ :
  ∀ (f : E → ℝ),
    (∃ (C : ℝ), ∀ (x y : E), dist (f x) (f y) ≤ C) →
      (∃ (L : NNReal), LipschitzWith L f) →
        Tendsto (β := ℝ)
          (fun (i : ι) ↦
            ∫ (ω : E),
              f
                ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X i) μ'') ⋯) :
                Measure E))
          l
          (𝓝
            (∫ (ω : E),
              f
                ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) :
                Measure E)))
⊢ Tendsto (β := ℝ)
    (fun (n : ι) ↦
      |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (X n) μ'') fun (ω : E) ↦ F ω)
          (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)|)
    l (𝓝 0)

Tactic:
simpa [tendsto_iff_dist_tendsto_zero] using hXZ F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩

Premises used: Exists.intro, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 ω)|
⊢ 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))

Tactic:
have h_tendsto :
      Tendsto (fun n ↦ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
        + |∫ ω, F ω ∂(μ''.map (X n)) - ∫ ω, F ω ∂(μ'.map Z)|) l (𝓝 (L * ε / 2)) := by
    suffices Tendsto (fun n ↦ L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
        + |∫ ω, F ω ∂(μ''.map (X n)) - ∫ ω, F ω ∂(μ'.map Z)|) l (𝓝 (L * ε / 2 + M * 0 + 0)) by
      simpa
    refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
    · rw [mul_div_assoc]
      exact tendsto_const_nhds
    · simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY
      exact hXY (ε / 2) (by positivity)
    · replace hXZ := hXZ.tendsto
      simp_rw [tendsto_iff_forall_lipschitz_integral_tendsto] at hXZ
      simpa [tendsto_iff_dist_tendsto_zero] using hXZ F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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))
⊢ 0 < (↑L : ℝ) * ε

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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))
⊢ (↑L : ℝ) * ε / 2 < (↑L : ℝ) * ε

Tactic:
have h_lt : L * ε / 2 < L * ε := half_lt_self (by positivity)
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
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 : ℝ) * ε
n : ι
hn :
  (↑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 : ℝ) * ε
⊢ |HSub.hSub (α := ℝ) (@integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω)
        (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω)| <
    (↑L : ℝ) * ε

Tactic:
(h_le n).trans_lt hn

Premises used: LE.le.trans_lt