awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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 μ'') ⋯
⊢ Eq (α := Measure E) (Measure.map Z μ') (Measure.map W μ'')
have h_eq₁ : (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry) : Measure E) =
  (↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map W μ'') sorry) : Measure E)
Tactic: rw [Subtype.ext_iff] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 (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) μ') ⋯))
have h₁ : ∀ (x : ι),
  Eq (α := { μ : Measure F // IsProbabilityMeasure μ })
    (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ X x) (μ x)) sorry)
    (ProbabilityMeasure.map (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (X x) (μ x)) sorry)
      sorry)
Tactic: convert! ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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)) ⋯) ⋯)
⊢ 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) μ') ⋯))
have h₂ : Eq (α := ProbabilityMeasure F)
  (Subtype.mk (p := fun (μ : Measure F) ↦ IsProbabilityMeasure μ) (Measure.map (g ∘ Z) μ') sorry)
  (ProbabilityMeasure.map (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry) sorry)
Tactic: convert! ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : ι
⊢ 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)) ⋯)
      ⋯)
have h₁ : Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map g (Measure.map (X x) (μ x)))
Tactic: simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk, Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 : ι
⊢ Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map g (Measure.map (X x) (μ x)))
have h₁ : Eq (α := Measure F) (Measure.map (g ∘ X x) (μ x)) (Measure.map (g ∘ X x) (μ x))
Tactic: rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable (h.forall_aemeasurable _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 μ μ'
⊢ 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 μ')) ⋯)
have h₁ : Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map g (Measure.map Z μ'))
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (goal)
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 μ μ'
⊢ Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map g (Measure.map Z μ'))
have h₁ : Eq (α := Measure F) (Measure.map (g ∘ Z) μ') (Measure.map (g ∘ Z) μ')
Tactic: rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable h.aemeasurable_limit]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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) μ''
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
have hZ : AEMeasurable Z μ'
Tactic: have hZ : AEMeasurable Z μ' := hXZ.aemeasurable_limit
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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 μ'
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
have hX : ∀ (i : ι), AEMeasurable (X i) μ''
Tactic: have hX : ∀ i, AEMeasurable (X i) μ'' := hXZ.forall_aemeasurable
-- 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) μ''
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
have inl : ∀ (hE : IsEmpty E),
  TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
Tactic: rcases isEmpty_or_nonempty E with hE | hE
-- 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) μ''
inl :
  ∀ (hE : IsEmpty 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 : ι) ↦ μ'') μ'
have inr : ∀ (hE : Nonempty E),
  TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
Tactic: rcases isEmpty_or_nonempty E with hE | hE
-- 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
⊢ TendstoInDistribution (Ω := fun (i : ι) ↦ Ω'') (m := fun (i : ι) ↦ m'') (mE := mE) Y l Z (fun (x : ι) ↦ μ'') μ'
have inr : Tendsto (fun (n : ι) ↦ Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map (Y n) μ'') sorry) l
  (𝓝 (Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry))
Tactic: refine ⟨hY, hZ, ?_⟩
-- 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
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 ω))
⊢ 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 μ') ⋯))
have 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) μ'') sorry) :
              Measure E))
        l
        (𝓝
          (∫ (ω : E),
            f ω ∂(↑(Subtype.mk (p := fun (μ : Measure E) ↦ IsProbabilityMeasure μ) (Measure.map Z μ') sorry) : Measure E)))
Tactic: rwa [tendsto_iff_forall_lipschitz_integral_tendsto]
-- 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
⊢ 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 μ') ⋯))
have 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 ω))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
have hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
Tactic: have hF_cont : Continuous F := hF_lip.continuous
-- 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
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
have inr : ∀ (hF_lip : LipschitzWith 0 F),
  Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
Tactic: obtain rfl | hL := eq_zero_or_pos L
Cleared hypotheses: L, hF_lip
-- 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
inr :
  ∀ (hF_lip : LipschitzWith 0 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 : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
have inr₁ : ∀ (hL : 0 < L),
  Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
Tactic: obtain rfl | hL := eq_zero_or_pos L
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hF_lip : LipschitzWith 0 F
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
have hF_lip₁ : ∀ (x y : E), F x = F y
Tactic: simp only [LipschitzWith.zero_iff] at hF_lip
Cleared hypotheses: hF_lip
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInDistribution (hypothesis)
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
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hF_lip : ∀ (x y : E), F x = F y
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ @integral _ _ _ _ mE (Measure.map (Y n) μ'') fun (ω : E) ↦ F ω) l
    (𝓝 (@integral _ _ _ _ mE (Measure.map Z μ') fun (ω : E) ↦ F ω))
have hF_lip₁ : ∀ (y : E), F x₀ = F y
Tactic: specialize hF_lip x₀
Cleared hypotheses: hF_lip