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 ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ρ.real (Set.Ioc 0 (↑N : ℝ)) ≤ ENNReal.toReal 1

Tactic:
ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one

Premises used: MeasureTheory.prob_le_one, MeasureTheory.Measure.real, ENNReal.toReal_mono, ENNReal.one_ne_top
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ρ.real (Set.Ioc 0 (↑N : ℝ)) ≤ ENNReal.toReal 1

Tactic:
exact ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one

Premises used: MeasureTheory.prob_le_one, ENNReal.toReal_mono, ENNReal.one_ne_top
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1

Tactic:
have A : ∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ ≤ 𝔼[X] + 1 :=
    calc
      ∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ =
          ∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ := by
        apply sum_congr rfl fun j hj => ?_
        rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]
        intro k _
        exact continuous_const.intervalIntegrable _ _
      _ = ∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ := by
        simp_rw [sum_sigma']
        refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
          aesop (add simp Nat.lt_succ_iff)
      _ ≤ ∑ i ∈ range N, (i + 1) * ∫ _ in i..(i + 1 : ℕ), (1 : ℝ) ∂ρ := by
        gcongr with i
        simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]
        refine mul_le_mul_of_nonneg_right (min_le_left _ _) ?_
        apply intervalIntegral.integral_nonneg
        · simp only [le_add_iff_nonneg_right, zero_le_one]
        · simp only [zero_le_one, imp_true_iff]
      _ ≤ ∑ i ∈ range N, ∫ x in i..(i + 1 : ℕ), x + 1 ∂ρ := by
        gcongr with i
        have I : (i : ℝ) ≤ (i + 1 : ℕ) := by
          simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]
        simp_rw [intervalIntegral.integral_of_le I, ← integral_const_mul]
        apply setIntegral_mono_on
        · exact continuous_const.integrableOn_Ioc
        · exact (continuous_id.add continuous_const).integrableOn_Ioc
        · exact measurableSet_Ioc
        · intro x hx
          simp only [Nat.cast_add, Nat.cast_one, Set.mem_Ioc] at hx
          simp [hx.1.le]
      _ = ∫ x in 0..N, x + 1 ∂ρ := by
        rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
        · norm_cast
        · exact (continuous_id.add continuous_const).intervalIntegrable _ _
      _ = ∫ x in 0..N, x ∂ρ + ∫ x in 0..N, 1 ∂ρ := by
        rw [intervalIntegral.integral_add]
        · exact continuous_id.intervalIntegrable _ _
        · exact continuous_const.intervalIntegrable _ _
      _ = 𝔼[truncation X N] + ∫ x in 0..N, 1 ∂ρ := by
        rw [integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]
      _ ≤ 𝔼[X] + ∫ x in 0..N, 1 ∂ρ := by
        grw [integral_truncation_le_integral_of_nonneg hint hnonneg]
      _ ≤ 𝔼[X] + 1 := by
        gcongr
        rw [intervalIntegral.integral_of_le (Nat.cast_nonneg _)]
        simp only [integral_const, measureReal_restrict_apply', measurableSet_Ioc, Set.univ_inter,
          smul_eq_mul, mul_one]
        rw [← ENNReal.toReal_one]
        exact ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
a b : ℝ
rw :
  Eq (α := ℝ≥0∞) (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} : ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.Ioc a b) : ℝ≥0∞)
⊢ ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
rw [ofReal_setIntegral_one ρ _,
      Measure.map_apply_of_aemeasurable hint.aemeasurable measurableSet_Ioc]

Premises used: MeasureTheory.Integrable.aemeasurable, MeasureTheory.ofReal_setIntegral_one, MeasureTheory.Measure.map_apply_of_aemeasurable, measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
a b : ℝ
⊢ Eq (α := ℝ≥0∞) (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} : ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.Ioc a b) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
⊢ ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
have B : ∀ a b, ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ _ in Set.Ioc a b, (1 : ℝ) ∂ρ) := by
    intro a b
    rw [ofReal_setIntegral_one ρ _,
      Measure.map_apply_of_aemeasurable hint.aemeasurable measurableSet_Ioc]
    rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ Eq (α := ℝ≥0∞)
    (∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    (∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ))

Tactic:
simp_rw [B]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)

Tactic:
simp [ENNReal.ofReal_sum_of_nonneg]

Premises used: ENNReal.ofReal_sum_of_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
e_r :
  Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
    (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
⊢ ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)

Tactic:
congr 1
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
    (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)

Tactic:
sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
e_r :
  ∀ (j : ℕ) (hj : j ∈ range K),
    Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
    (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)

Tactic:
refine sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j : ℕ
hj : j ∈ range K
e_r e_r₁ : Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)

Tactic:
rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]

Premises used: Iff.mpr, LT.lt.le, Finset.mem_range, intervalIntegral.integral_of_le, Iff.mp, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ) ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)

Tactic:
ENNReal.ofReal_le_ofReal A

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j :
  Eq (α := ℝ≥0∞)
    (∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    (∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ))
j₁ :
  ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
j₂ :
  ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
⊢ ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)

Tactic:
calc
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A

Premises used: Set.Ioc, ENNReal.ofReal, intervalIntegral, ENNReal.ofReal_le_ofReal, MeasureTheory.Measure.restrict, Nat.cast, Finset.range, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, MeasureTheory.integral, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
suffices :
  ∀ (K : ℕ),
    ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)} ≤
      ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ), ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)})
    ∞

Tactic:
suffices ∀ K : ℕ, ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)} ≤ ENNReal.ofReal (𝔼[X] + 1) from
    (le_of_tendsto_of_tendsto (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds
      (Eventually.of_forall this)).trans_lt ENNReal.ofReal_lt_top
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    atTop
    (𝓝
      (∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))

Tactic:
tendsto_finsetSum _ fun i _ => ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K : ℕ
refine :
  ∀ i ∈ range K,
    Tendsto (β := ℝ≥0∞)
      (fun (N : ℕ) ↦
        (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
          ℝ≥0∞))
      atTop
      (𝓝 (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}) :
        Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    atTop
    (𝓝
      (∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))

Tactic:
refine tendsto_finsetSum _ fun i _ => ?_

Premises used: tendsto_finsetSum
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
apply :
  Subset.{u_1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
apply₁ :
  Subset.{u_1} (α := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
    {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})

Tactic:
apply Set.Subset.antisymm _ _

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)} ω
⊢ ∃ (N : ℕ), X ω ≤ (↑N : ℝ)

Tactic:
exists_nat_ge (X ω)

Premises used: exists_nat_ge
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)} ω
obtain :
  ∀ (N : ℕ) (hN : X ω ≤ (↑N : ℝ)),
    Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω
⊢ Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)

Premises used: exists_nat_ge
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)} ω
N : ℕ
hN : X ω ≤ (↑N : ℝ)
⊢ Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω

Tactic:
Set.mem_iUnion.2 ⟨N, hω, hN⟩

Premises used: Iff.mpr, Set.mem_iUnion, And.intro, Exists.intro
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)} ω
N : ℕ
hN : X ω ≤ (↑N : ℝ)
⊢ Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω

Tactic:
exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
⊢ Subset.{u_1} (α := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
    {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}

Tactic:
simp +contextual only [Set.mem_Ioc, Set.mem_Ioi,
          Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]

Premises used: Set.iUnion_subset_iff, Set.mem_Ioi, imp_true_iff, Set.setOf_subset_setOf, Set.mem_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})

Tactic:
have : {ω | X ω ∈ Set.Ioi (i : ℝ)} = ⋃ N : ℕ, {ω | X ω ∈ Set.Ioc (i : ℝ) N} := by
      apply Set.Subset.antisymm _ _
      · intro ω hω
        obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
        exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
      · simp +contextual only [Set.mem_Ioc, Set.mem_Ioi,
          Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
rw :
  Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝
        (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})) :
      Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝 (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}) :
      Filter ℝ≥0∞)

Tactic:
rw [this]