awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
m n : ℕ
hmn : m ≤ n
⊢ LE.le (α := ℝ) ((fun (n : ℕ) ↦ (∑ i ∈ range n, X i ω : ℝ)) m) ((fun (n : ℕ) ↦ (∑ i ∈ range n, X i ω : ℝ)) n)

Tactic:
exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω

Premises used: Finset.sum_le_sum_of_subset_of_nonneg, Finset.range_mono
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
exact hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
pos :
  ∀ (h : ∀ᵐ (ω : Ω), X 0 ω = 0),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), X 0 x ∂μ))
neg :
  ∀ (h : ¬∀ᵐ (ω : Ω), X 0 ω = 0),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by_cases h : ∀ᵐ ω, X 0 ω = 0
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
h₁ :
  ∀ (ω : Ω) (hω : ∀ (i : ℕ), X i ω = 0),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [I] with ω hω
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) 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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
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_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
⊢ Measurable pos

Tactic:
have posm : Measurable pos := measurable_id'.max measurable_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
⊢ Measurable neg

Tactic:
have negm : Measurable neg := measurable_id'.neg.max measurable_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))

Tactic:
have A : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (pos ∘ X i) ω) / n) atTop (𝓝 𝔼[pos ∘ X 0]) :=
    strong_law_aux7 _ hint.pos_part (fun i j hij => (hindep hij).comp posm posm)
      (fun i => (hident i).comp posm) fun i ω => le_max_right _ _
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))

Tactic:
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (neg ∘ X i) ω) / n) atTop (𝓝 𝔼[neg ∘ X 0]) :=
    strong_law_aux7 _ hint.neg_part (fun i j hij => (hindep hij).comp negm negm)
      (fun i => (hident i).comp negm) fun i ω => le_max_right _ _
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
h₁ :
  ∀ (ω : Ω)
    (hωpos :
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)))
    (hωneg :
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [A, B] with ω hωpos hωneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
⊢ Tendsto
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (pos ∘ X i) ω) (↑x : ℝ) -
        HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (neg ∘ X i) ω) (↑x : ℝ))
    atTop
    (𝓝
      (HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a)))

Tactic:
hωpos.sub hωneg

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
h₁ :
  ∀ (x : ℕ),
    HDiv.hDiv (α := ℝ) (∑ i ∈ range x, X i ω) (↑x : ℝ) =
      HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (pos ∘ X i) ω) (↑x : ℝ) -
        HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (neg ∘ X i) ω) (↑x : ℝ)
h₂ :
  ∫ (x : Ω), X 0 x ∂μ =
    HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
convert! hωpos.sub hωneg using 2

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
x : ℕ
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ range x, X i ω) (↑x : ℝ) =
    HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (pos ∘ X i) ω) (↑x : ℝ) -
      HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (neg ∘ X i) ω) (↑x : ℝ)

Tactic:
simp only [pos, neg, ← sub_div, ← sum_sub_distrib, max_zero_sub_max_neg_zero_eq_self,
      Function.comp_apply]

Premises used: sub_div, max_zero_sub_max_neg_zero_eq_self, Finset.sum_sub_distrib, Function.comp_apply
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
⊢ ∫ (x : Ω), X 0 x ∂μ =
    HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a)

Tactic:
simp +instances only [pos, neg, ← integral_sub hint.pos_part hint.neg_part,
      max_zero_sub_max_neg_zero_eq_self, Function.comp_apply, mΩ]

Premises used: MeasureTheory.Integrable.neg_part, MeasureTheory.integral_sub, max_zero_sub_max_neg_zero_eq_self, MeasureTheory.Integrable.pos_part, Function.comp_apply
-- 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
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))

Tactic:
SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ

Premises used: MeasureTheory.SimpleFunc.induction
-- 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
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
refine_1 :
  ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
    (fun (ψ : SimpleFunc E E) ↦
        ∀ᵐ (ω : Ω) ∂μ,
          Tendsto.{0, u_2} (β := E)
            (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
            atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
      (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0))
refine_2 :
  ∀ ⦃f g : SimpleFunc E E⦄,
    Disjoint (α := Set E) (Function.support (M := E) (⇑f : (a : E) → E))
        (Function.support (M := E) (⇑g : (a : E) → E)) →
      (fun (ψ : SimpleFunc E E) ↦
            ∀ᵐ (ω : Ω) ∂μ,
              Tendsto.{0, u_2} (β := E)
                (fun (n : ℕ) ↦
                  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
          f →
        (fun (ψ : SimpleFunc E E) ↦
              ∀ᵐ (ω : Ω) ∂μ,
                Tendsto.{0, u_2} (β := E)
                  (fun (n : ℕ) ↦
                    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                  atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
            g →
          (fun (ψ : SimpleFunc E E) ↦
              ∀ᵐ (ω : Ω) ∂μ,
                Tendsto.{0, u_2} (β := E)
                  (fun (n : ℕ) ↦
                    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                  atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
            (f + g)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))

Tactic:
refine SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ

Premises used: MeasureTheory.SimpleFunc.induction