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 ρ
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
      Eq (α := ℝ) (∫ (x : ℝ) in (↑(a.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(a.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
        (∫ (x : ℝ) in
          (↑(Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                ((fun (p : (_ : ℕ) × ℕ) ↦
                    (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                      (_ : ℕ) × ℕ))
                  a)) :
            ℝ)..(↑(HAdd.hAdd (α := ℕ)
                (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                  ((fun (p : (_ : ℕ) × ℕ) ↦
                      (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                        (_ : ℕ) × ℕ))
                    a))
                1) :
            ℝ),
          1 ∂ρ)

Tactic:
aesop (add simp Nat.lt_succ_iff)

Premises used: Nat.lt_succ_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 N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
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 ∂ρ
⊢ 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 ∂ρ)

Tactic:
gcongr with i
-- 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 ρ
i : ℕ
h_1 : i ∈ range N
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 ∂ρ
⊢ ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ

Tactic:
simp only [Nat.cast_add, Nat.cast_one, sum_const, card_range, nsmul_eq_mul, Nat.cast_min]

Premises used: Finset.card_range, Nat.cast_min, Nat.cast_add, nsmul_eq_mul, Nat.cast_one, Finset.sum_const
-- 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 ρ
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 ∂ρ

Tactic:
mul_le_mul_of_nonneg_right (min_le_left _ _) ?_

Premises used: min_le_left, mul_le_mul_of_nonneg_right
-- 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 ρ
i : ℕ
h_1 : i ∈ range N
h : LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ)
⊢ 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:
refine mul_le_mul_of_nonneg_right (min_le_left _ _) ?_

Premises used: min_le_left, mul_le_mul_of_nonneg_right
-- 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 ρ
i : ℕ
h_1 : i ∈ range N
h : (↑i : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
h₁ : ∀ u ∈ Set.Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑i : ℝ)..HAdd.hAdd (α := ℝ) (↑i : ℝ) 1, 1 ∂ρ)

Tactic:
apply intervalIntegral.integral_nonneg

Premises used: intervalIntegral.integral_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 ρ
i : ℕ
h : i ∈ range N
⊢ (↑i : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

Premises used: le_add_iff_nonneg_right, zero_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 ρ
i : ℕ
h : i ∈ range N
⊢ ∀ u ∈ Set.Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), LE.le (α := ℝ) 0 1

Tactic:
simp only [zero_le_one, imp_true_iff]

Premises used: zero_le_one, 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 N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
h :
  ∀ i ∈ range N,
    HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
      ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ
⊢ 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 ∂ρ)

Tactic:
gcongr with i
-- 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 ρ
i : ℕ
h : i ∈ range N
⊢ LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]

Premises used: le_add_iff_nonneg_right, zero_le_one, Nat.cast_add, Nat.cast_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 ρ
i : ℕ
h : i ∈ range N
⊢ 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]
-- 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 ρ
i : ℕ
h_1 : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
h :
  LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ ≤
    ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ

Tactic:
simp_rw [intervalIntegral.integral_of_le I, ← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, intervalIntegral.integral_of_le
-- 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 ρ
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) : ℝ))
h₃ :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) x → HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ≤ x + 1
⊢ LE.le (α := ℝ) (∫ (a : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ), x + 1 ∂ρ)

Tactic:
apply setIntegral_mono_on

Premises used: MeasureTheory.setIntegral_mono_on
-- 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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ

Tactic:
continuous_const.integrableOn_Ioc

Premises used: continuous_const, Continuous.integrableOn_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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ

Tactic:
exact continuous_const.integrableOn_Ioc

Premises used: continuous_const, Continuous.integrableOn_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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ x + 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ

Tactic:
(continuous_id.add continuous_const).integrableOn_Ioc

Premises used: continuous_const, continuous_id, Continuous.integrableOn_Ioc, Continuous.add
-- 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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ x + 1) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) ρ

Tactic:
exact (continuous_id.add continuous_const).integrableOn_Ioc

Premises used: continuous_const, continuous_id, Continuous.integrableOn_Ioc, Continuous.add
-- 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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ MeasurableSet (α := ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ))

Tactic:
measurableSet_Ioc

Premises used: 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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
⊢ MeasurableSet (α := ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ))

Tactic:
exact measurableSet_Ioc

Premises used: 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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ (↑i : ℝ) < x ∧ x ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
simp only [Nat.cast_add, Nat.cast_one, Set.mem_Ioc] at hx

Premises used: Nat.cast_add, Set.mem_Ioc, Nat.cast_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 ρ
i : ℕ
h : i ∈ range N
I : LE.le (α := ℝ) (↑i : ℝ) (↑(i + 1) : ℝ)
x : ℝ
hx : (↑i : ℝ) < x ∧ x ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * 1 ≤ x + 1

Tactic:
simp [hx.1.le]

Premises used: LT.lt.le, And.left
-- 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 ρ
rw : Eq (α := ℝ) (∫ (x : ℝ) in (↑0 : ℝ)..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
rw₁ : ∀ k < N, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x + 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ range N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]

Premises used: intervalIntegral.sum_integral_adjacent_intervals
-- 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 ρ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑0 : ℝ)..(↑N : ℝ), x + 1 ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ)

Tactic:
norm_cast
-- 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 ρ
k : ℕ
h : k < N
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x + 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
(continuous_id.add continuous_const).intervalIntegrable _ _

Premises used: continuous_const, Continuous.intervalIntegrable, continuous_id, Continuous.add
-- 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 ρ
k : ℕ
h : k < N
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x + 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
exact (continuous_id.add continuous_const).intervalIntegrable _ _

Premises used: continuous_const, Continuous.intervalIntegrable, continuous_id, Continuous.add
-- 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 ρ
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) ρ 0 (↑N : ℝ)
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ 0 (↑N : ℝ)
⊢ ∫ (x : ℝ) in 0..(↑N : ℝ), x + 1 ∂ρ =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), x ∂ρ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ)

Tactic:
rw [intervalIntegral.integral_add]

Premises used: intervalIntegral.integral_add
-- 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 ρ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) ρ 0 (↑N : ℝ)

Tactic:
continuous_id.intervalIntegrable _ _

Premises used: Continuous.intervalIntegrable, continuous_id
-- 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 ρ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x) ρ 0 (↑N : ℝ)

Tactic:
exact continuous_id.intervalIntegrable _ _

Premises used: Continuous.intervalIntegrable, continuous_id
-- 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 ρ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ 0 (↑N : ℝ)

Tactic:
continuous_const.intervalIntegrable _ _

Premises used: continuous_const, Continuous.intervalIntegrable
-- 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 ρ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ 0 (↑N : ℝ)

Tactic:
exact continuous_const.intervalIntegrable _ _

Premises used: continuous_const, Continuous.intervalIntegrable
-- 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 ρ
rw 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 ∂ρ)
⊢ 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 ∂ρ)

Tactic:
rw [integral_truncation_eq_intervalIntegral_of_nonneg hint.1 hnonneg]

Premises used: ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg, And.left
-- 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 ρ
grw 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 ∂ρ)
⊢ 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 ∂ρ)

Tactic:
grw [integral_truncation_le_integral_of_nonneg hint hnonneg]

Premises used: ProbabilityTheory.integral_truncation_le_integral_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 ρ
bc : LE.le (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) 1
⊢ HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a)
      (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1

Tactic:
gcongr
-- 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 ρ
bc : LE.le (α := ℝ) (∫ (x : ℝ) in Set.Ioc 0 (↑N : ℝ), 1 ∂ρ) 1
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..(↑N : ℝ), 1 ∂ρ) 1

Tactic:
rw [intervalIntegral.integral_of_le (Nat.cast_nonneg _)]

Premises used: Nat.cast_nonneg, intervalIntegral.integral_of_le
-- 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 ρ
bc : ρ.real (Set.Ioc 0 (↑N : ℝ)) ≤ 1
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in Set.Ioc 0 (↑N : ℝ), 1 ∂ρ) 1

Tactic:
simp only [integral_const, measureReal_restrict_apply', measurableSet_Ioc, Set.univ_inter,
          smul_eq_mul, mul_one]

Premises used: MeasureTheory.measureReal_restrict_apply', Set.univ_inter, MeasureTheory.integral_const, smul_eq_mul, mul_one, measurableSet_Ioc