awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ Integrable (Y k 0) μ

Tactic:
((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ Integrable (Y k 0) μ

Tactic:
exact ((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ

Tactic:
have : ‖μ[Y k 0] - μ[X 0]‖ < δ := by
    rw [norm_sub_rev, ← integral_sub hint]
    · exact (norm_integral_le_integral_norm _).trans_lt hk
    · exact ((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
⊢ ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ

Tactic:
have I : ∀ᶠ n in atTop, (∑ i ∈ range n, ‖(X i - Y k i) ω‖) / n < δ :=
    (tendsto_order.1 (h'ω k)).2 δ hk
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
    atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))

Tactic:
specialize hω k
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
hω :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
    atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
⊢ Tendsto (β := ℝ)
    (fun (e : ℕ) ↦ ‖HSMul.hSMul (α := ℝ) (β := E) (↑e : ℝ)⁻¹ (∑ i ∈ Finset.range e, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖)
    atTop (𝓝 0)

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero] at hω

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
hω :
  Tendsto (β := ℝ)
    (fun (e : ℕ) ↦ ‖HSMul.hSMul (α := ℝ) (β := E) (↑e : ℝ)⁻¹ (∑ i ∈ Finset.range e, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖)
    atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ

Tactic:
(tendsto_order.1 hω).2 δ δpos

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
hω :
  Tendsto (β := ℝ)
    (fun (e : ℕ) ↦ ‖HSMul.hSMul (α := ℝ) (β := E) (↑e : ℝ)⁻¹ (∑ i ∈ Finset.range e, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖)
    atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ

Tactic:
exact (tendsto_order.1 hω).2 δ δpos

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
⊢ ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ

Tactic:
have J : ∀ᶠ (n : ℕ) in atTop, ‖(n : ℝ)⁻¹ • (∑ i ∈ range n, Y k i ω) - μ[Y k 0]‖ < δ := by
    specialize hω k
    rw [tendsto_iff_norm_sub_tendsto_zero] at hω
    exact (tendsto_order.1 hω).2 δ δpos
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
J :
  ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
h :
  ∀ (n : ℕ) (hn : HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ)
    (h'n : ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ),
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
⊢ ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε

Tactic:
filter_upwards [I, J] with n hn h'n