awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
refine_1 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N)
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_3 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
      (fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (p : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N,
      ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
    (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K),
      ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
have refine_4 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
      ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K)) a →
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a) =
      a
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ LE.le (α := ℝ) (∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
    (∑ i ∈ range N, HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
have h : ∀ i ∈ range N,
  ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h : i ∈ range N
⊢ ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ
have h : min (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) (↑K : ℝ) * ∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ ≤
  HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ
Tactic: simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h : i ∈ range N
⊢ min (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) (↑K : ℝ) * ∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ
have h : LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ)
Tactic: refine mul_le_mul_of_nonneg_right (min_le_left _ _) ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h : i ∈ range N
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ)
have h : (↑i : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: apply intervalIntegral.integral_nonneg
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h_1 : i ∈ range N
h : (↑i : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ)
have h₁ : ∀ u ∈ Set.Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), LE.le (α := ℝ) 0 1
Tactic: apply intervalIntegral.integral_nonneg
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ LE.le (α := ℝ) (∑ i ∈ range N, HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
    (∑ i ∈ range N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ)
have h : ∀ i ∈ range N,
  HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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 ρ
i : ℕ
h : i ∈ range N
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ
have I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
Tactic: have I : (i : ℝ) ≤ (i + 1 : ℕ) := by
          simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ
have h : LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
  (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
Tactic: simp_rw [intervalIntegral.integral_of_le I, ← integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
have h : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h_1 : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
h : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
⊢ LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
have h₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ x + 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h_1 : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
h : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
h₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ x + 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
⊢ LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
have h₂ : MeasurableSet (α := ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ))
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
i : ℕ
h_1 : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
h : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
h₁ : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ x + 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ
h₂ : MeasurableSet (α := ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ))
⊢ LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
have h₃ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) x → HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ≤ x + 1
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ≤ x + 1
have hx₁ : (↑i : ℝ) < x ∧ x ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: simp only [Nat.cast_add, Nat.cast_one, Set.mem_Ioc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ Eq (α := ℝ) (∑ i ∈ range N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
have rw : Eq (α := ℝ) (∫ (x : ℝ) in (↑0 : ℝ)..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
rw : Eq (α := ℝ) (∫ (x : ℝ) in (↑0 : ℝ)..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
⊢ Eq (α := ℝ) (∑ i ∈ range N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
have rw₁ : ∀ k < N, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x + 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑0 : ℝ)..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
have norm_cast : Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ ∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) ρ 0 (↑N : ℝ)
Tactic: rw [intervalIntegral.integral_add]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) ρ 0 (↑N : ℝ)
⊢ ∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ 0 (↑N : ℝ)
Tactic: rw [intervalIntegral.integral_add]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) =
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation X (↑N : ℝ) a)
      (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) =
  HAdd.hAdd (α := ℝ) (∫ (y : ℝ) in 0..(↑N : ℝ), y ∂Measure.map X ℙ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
Tactic: rw [integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation X (↑N : ℝ) a)
      (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a)
      (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
have grw : HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ X x)
    (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) ≤
  HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ X x)
    (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)
Tactic: grw [integral_truncation_le_integral_of_nonneg hint hnonneg]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a)
      (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
have bc : LE.le (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) 1
have bc : LE.le (α := ℝ) (∫ (x : ℝ) in Set.Ioc 0 (↑N : ℝ), 1 ∂ρ) 1
Tactic: rw [intervalIntegral.integral_of_le (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ρ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in Set.Ioc 0 (↑N : ℝ), 1 ∂ρ) 1
have bc : ρ.real (Set.Ioc 0 (↑N : ℝ)) ≤ 1
Tactic: simp only [integral_const, measureReal_restrict_apply', measurableSet_Ioc, Set.univ_inter,
          smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ∂ρ)
have rw : Eq (α := ℝ≥0∞) (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} : ℝ≥0∞)
  (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' Set.Ioc a b) : ℝ≥0∞)
Tactic: rw [ofReal_setIntegral_one ρ _,
      Measure.map_apply_of_aemeasurable hint.aemeasurable measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
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
⊢ ∑ 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)
have B : ∀ (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
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
have e_r : Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
  (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
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 ∂ρ)
have e_r : ∀ (j : ℕ) (hj : j ∈ range K),
  Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
Tactic: refine sum_congr rfl fun j hj => ?_