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_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ :
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯
⊢ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯

Tactic:
rw! [Measure.map_congr hZT]

Premises used: MeasureTheory.Measure.map_congr
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᶠ[ae (μ i)] Y i
hZT : Z =ᶠ[ae μ'] T
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
⊢ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map T μ') ⋯

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : IsEmpty E
simp :
  Tendsto (β := ProbabilityMeasure E) (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯)
    l (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯))
⊢ Tendsto (β := ProbabilityMeasure E)
    (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
simp only [Subsingleton.elim _ (0 : Measure E)]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : IsEmpty E
⊢ Tendsto (β := ProbabilityMeasure E) (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯)
    l (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯))

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_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
inst_3 : IsEmpty E
⊢ Tendsto (β := ProbabilityMeasure E) (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯)
    l (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) 0 ⋯))

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
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_2 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_3 : TopologicalSpace E
inst_4 : HasOuterApproxClosed E
inst_5 : BorelSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
W : Ω'' → E
inst_6 : l.NeBot
h1 : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h2 : TendstoInDistribution (Ω := Ω) (mE := mE) X l W μ μ''
⊢ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') ⋯

Tactic:
have h_eq := tendsto_nhds_unique h1.tendsto h2.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_2 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_3 : TopologicalSpace E
inst_4 : HasOuterApproxClosed E
inst_5 : BorelSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
W : Ω'' → E
inst_6 : l.NeBot
h1 : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h2 : TendstoInDistribution (Ω := Ω) (mE := mE) X l W μ μ''
h_eq :
  Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯ =
    Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') ⋯
⊢ (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) : Measure E) =
    (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') ⋯) : Measure E)

Tactic:
rw [Subtype.ext_iff] at h_eq

Premises used: Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst_2 : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst_3 : TopologicalSpace E
inst_4 : HasOuterApproxClosed E
inst_5 : BorelSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
W : Ω'' → E
inst_6 : l.NeBot
h1 : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h2 : TendstoInDistribution (Ω := Ω) (mE := mE) X l W μ μ''
h_eq :
  (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) : Measure E) =
    (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') ⋯) : Measure E)
⊢ Eq (α := Measure E) (Measure.map Z μ') (Measure.map W μ'')

Tactic:
simpa using h_eq
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
⊢ Tendsto (β := ProbabilityMeasure F)
    (fun (i : ι) ↦
      ProbabilityMeasure.map
        (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X i) (μ i)) ⋯) ⋯)
    l
    (𝓝 (ProbabilityMeasure.map (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) ⋯))

Tactic:
ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous, MeasureTheory.TendstoInDistribution.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ :
  ∀ (x : ι),
    Eq (α := { μ : Measure F // IsProbabilityMeasure μ })
      (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ X x) (μ x)) ⋯)
      (ProbabilityMeasure.map
        (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X x) (μ x)) ⋯) ⋯)
h₂ :
  Eq (α := ProbabilityMeasure F)
    (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ Z) μ') ⋯)
    (ProbabilityMeasure.map (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) ⋯)
⊢ Tendsto (β := ProbabilityMeasure F)
    (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ X n) (μ n)) ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ Z) μ') ⋯))

Tactic:
convert! ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous, MeasureTheory.TendstoInDistribution.tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
x : ι
h₁ : Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map g (Measure.map (X x) (μ x)))
⊢ Eq (α := { μ : Measure F // IsProbabilityMeasure μ })
    (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ X x) (μ x)) ⋯)
    (ProbabilityMeasure.map (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X x) (μ x)) ⋯)
      ⋯)

Tactic:
simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk, Subtype.mk.injEq]

Premises used: MeasureTheory.ProbabilityMeasure.coe_mk, Subtype.mk.injEq, MeasureTheory.ProbabilityMeasure.map
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
x : ι
h₁ h₂ : Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map (g ∘ X x) (μ x))
⊢ Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map g (Measure.map (X x) (μ x)))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable (h.forall_aemeasurable _)]

Premises used: MeasureTheory.TendstoInDistribution.forall_aemeasurable, Continuous.aemeasurable, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ : Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map g (Measure.map Z μ'))
⊢ Eq (α := ProbabilityMeasure F)
    (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ Z) μ') ⋯)
    (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map g (Measure.map Z μ')) ⋯)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution
Goal:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst_1 : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst_2 : TopologicalSpace E
F : Type u_6
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
g : E → F
hg : Continuous[inst_2, inst_4] g
h : TendstoInDistribution (Ω := Ω) (mE := mE) X l Z μ μ'
h₁ h₂ : Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map (g ∘ Z) μ')
⊢ Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map g (Measure.map Z μ'))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable h.aemeasurable_limit]

Premises used: Continuous.aemeasurable, MeasureTheory.TendstoInDistribution.aemeasurable_limit, AEMeasurable.map_map_of_aemeasurable
-- 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) μ''
⊢ AEMeasurable Z μ'

Tactic:
have hZ : AEMeasurable Z μ' := hXZ.aemeasurable_limit
-- 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 μ'
⊢ ∀ (i : ι), AEMeasurable (X i) μ''

Tactic:
have hX : ∀ i, AEMeasurable (X i) μ'' := hXZ.forall_aemeasurable
-- 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) μ''
inl :
  ∀ (hE : IsEmpty E),
    TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
inr :
  ∀ (hE : Nonempty E),
    TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'

Tactic:
rcases isEmpty_or_nonempty E with hE | hE

Premises used: isEmpty_or_nonempty
-- 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 : IsEmpty E
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'

Tactic:
simp
-- 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
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'

Tactic:
⟨hY, hZ, ?_⟩

Premises used: MeasureTheory.TendstoInDistribution.mk
-- 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
inr :
  Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'

Tactic:
refine ⟨hY, hZ, ?_⟩
-- 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
this :
  ∀ (F : E → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ (x y : E), dist (F x) (F y) ≤ C)
    (hF_lip : ∃ (L : NNReal), LipschitzWith L F),
    Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
      (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (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 (Y i) μ'') ⋯) :
                Measure E))
          l
          (𝓝
            (∫ (ω : E),
              f
                ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯) :
                Measure E)))
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
rwa [tendsto_iff_forall_lipschitz_integral_tendsto]

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 : 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
inr :
  ∀ (F : E → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ (x y : E), dist (F x) (F y) ≤ C)
    (hF_lip : ∃ (L : NNReal), LipschitzWith L F),
    Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
      (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
⊢ Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) μ'') ⋯) l
    (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') ⋯))

Tactic:
suffices ∀ (F : E → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ x y, dist (F x) (F y) ≤ C)
      (hF_lip : ∃ L, LipschitzWith L F),
      Tendsto (fun n ↦ ∫ ω, F ω ∂(μ''.map (Y n))) l (𝓝 (∫ ω, F ω ∂(μ'.map Z))) by
    rwa [tendsto_iff_forall_lipschitz_integral_tendsto]