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_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 ∂μ‖ < δ
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 ∂μ‖ < δ
⊢ norm.{u_2} (E := E) (∑ i ∈ Finset.range n, (X i ω - Y k i ω)) ≤ ∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖

Tactic:
exact norm_sum_le _ _

Premises used: norm_sum_le
-- 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 ∂μ‖ < δ
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 ∂μ‖ < δ
bc : HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) (↑n : ℝ) ≤ δ
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) (↑n : ℝ) + δ + δ ≤ δ + δ + δ

Tactic:
gcongr
-- 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 ∂μ‖ < δ
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 ∂μ‖ < δ
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) (↑n : ℝ) ≤ δ

Tactic:
hn.le

Premises used: LT.lt.le
-- 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 ∂μ‖ < δ
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 ∂μ‖ < δ
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) (↑n : ℝ) ≤ δ

Tactic:
exact hn.le

Premises used: LT.lt.le
-- 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 ∂μ‖ < δ
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 ∂μ‖ < δ
⊢ δ + δ + δ < ε

Tactic:
hδ
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
pos :
  ∀ (h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
        atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
neg :
  ∀ (h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
        atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
rw : ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, X i a = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
i : ℕ
⊢ ∀ᵐ (a : Ω) ∂μ, X i a = 0

Tactic:
(hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.ae_snd, measurableSet_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
i : ℕ
⊢ ∀ᵐ (a : Ω) ∂μ, X i a = 0

Tactic:
exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.ae_snd, measurableSet_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
h₁ :
  ∀ (ω : Ω) (hω : ∀ (i : ℕ), X i ω = 0),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [I] with ω hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω)) atTop
    (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
simpa [hω] using (integral_eq_zero_of_ae h).symm

Premises used: MeasureTheory.integral_eq_zero_of_ae, Eq.symm
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ :=
    hint.isProbabilityMeasure_of_indepFun (X 0) (X 1) h (hindep zero_ne_one)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
⊢ ∀ (i : ℕ), Integrable (X i) μ

Tactic:
have A : ∀ i, Integrable (X i) μ := fun i ↦ (hident i).integrable_iff.2 hint
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω

Tactic:
have B : ∀ᵐ ω ∂μ, ∀ n, X n ω = Y n ω :=
    ae_all_iff.2 (fun i ↦ AEStronglyMeasurable.ae_eq_mk (A i).1)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
⊢ Integrable (Y 0) μ

Tactic:
have Yint : Integrable (Y 0) μ := Integrable.congr hint (AEStronglyMeasurable.ae_eq_mk (A 0).1)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
apply strong_law_ae_of_measurable Y Yint ((A 0).1.stronglyMeasurable_mk)
      (fun i j hij ↦ IndepFun.congr (hindep hij) (A i).1.ae_eq_mk (A j).1.ae_eq_mk)
      (fun i ↦ ((A i).1.identDistrib_mk.symm.trans (hident i)).trans (A 0).1.identDistrib_mk)

Premises used: MeasureTheory.AEStronglyMeasurable.identDistrib_mk, ProbabilityTheory.IndepFun.congr, ProbabilityTheory.IdentDistrib.symm, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.strong_law_ae_of_measurable, OfNat.ofNat
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
have C : ∀ᵐ ω ∂μ,
      Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y i ω)) atTop (𝓝 μ[Y 0]) := by
    apply strong_law_ae_of_measurable Y Yint ((A 0).1.stronglyMeasurable_mk)
      (fun i j hij ↦ IndepFun.congr (hindep hij) (A i).1.ae_eq_mk (A j).1.ae_eq_mk)
      (fun i ↦ ((A i).1.identDistrib_mk.symm.trans (hident i)).trans (A 0).1.identDistrib_mk)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun (i : ℕ) ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
C :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
      atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
h₁ :
  ∀ (ω : Ω) (h₁ : ∀ (n : ℕ), X n ω = Y n ω)
    (h₂ :
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y i ω))
        atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [B, C] with ω h₁ h₂