awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
inr :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
        (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
inr₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)

Tactic:
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']

Premises used: MeasureTheory.integral_indicator, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.integral_map, LT.lt.le, intervalIntegral.integral_of_ge
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
inr :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
    0
⊢ Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
        (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)

Tactic:
simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]

Premises used: zero_eq_neg, LT.lt.le, Set.indicator_empty, Set.Ioc_eq_empty_of_le, MeasureTheory.integral_zero, zero_pow
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
inr : (ae (F := Measure ℝ) (Measure.map f μ)).EventuallyEq (β := ℝ) ((Set.Ioc A 0).indicator fun (x : ℝ) ↦ x ^ n) 0
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
    0

Tactic:
apply integral_eq_zero_of_ae

Premises used: MeasureTheory.integral_eq_zero_of_ae
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x

Tactic:
have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
h : ∀ (x : ℝ) (hx : 0 ≤ x), Eq (α := ℝ) ((Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x) (0 x)
⊢ (ae (F := Measure ℝ) (Measure.map f μ)).EventuallyEq (β := ℝ) ((Set.Ioc A 0).indicator fun (x : ℝ) ↦ x ^ n) 0

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x → x ≤ 0 → x ^ n = 0
⊢ Eq (α := ℝ) ((Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x) (0 x)

Tactic:
simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]

Premises used: Set.indicator, and_imp, Pi.zero_apply, ite_eq_right_iff, Set.mem_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
linarith : x < 0 → 0 - x + (x - 0) = 0
linarith₁ : 0 < x → x - 0 + (0 - x) = 0
⊢ x = 0

Tactic:
linarith
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
⊢ x = 0

Tactic:
have : x = 0 := by linarith
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this_1 : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
this : x = 0
⊢ x ^ n = 0

Tactic:
simp [this, zero_pow hn]

Premises used: zero_pow
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ∂μ) (∫ (y : ℝ) in -A..A, y ∂Measure.map f μ)

Tactic:
simpa using moment_truncation_eq_intervalIntegral hf hA one_ne_zero

Premises used: ProbabilityTheory.moment_truncation_eq_intervalIntegral, one_ne_zero
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ∂μ) (∫ (y : ℝ) in 0..A, y ∂Measure.map f μ)

Tactic:
simpa using moment_truncation_eq_intervalIntegral_of_nonneg hf one_ne_zero h'f

Premises used: ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, one_ne_zero
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
apply : ∀ (x : α), 0 x ≤ truncation f A x
apply₁ : ∀ (x : α), truncation f A x ≤ f x
⊢ LE.le (α := ℝ) (∫ (x : α), truncation f A x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
apply integral_mono_of_nonneg
    (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ 0 x ≤ truncation f A x

Tactic:
truncation_nonneg _ (h'f x)

Premises used: ProbabilityTheory.truncation_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ 0 x ≤ truncation f A x

Tactic:
exact truncation_nonneg _ (h'f x)

Premises used: ProbabilityTheory.truncation_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ |truncation f A x|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
abs_truncation_le_abs_self _ _ _

Premises used: ProbabilityTheory.abs_truncation_le_abs_self
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ |f x| = f x

Tactic:
abs_of_nonneg (h'f x)

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ f x

Tactic:
calc
      truncation f A x ≤ |truncation f A x| := le_abs_self _
      _ ≤ |f x| := abs_truncation_le_abs_self _ _ _
      _ = f x := abs_of_nonneg (h'f x)

Premises used: le_abs_self, abs_of_nonneg, ProbabilityTheory.abs_truncation_le_abs_self, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_

Premises used: abs, MeasureTheory.tendsto_integral_filter_of_dominated_convergence
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
refine_2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a
refine_3 : Integrable (ε := ℝ) (fun (x : α) ↦ |f x|) μ
refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℝ) ↦ truncation f n a) atTop (𝓝 (f a))
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_

Premises used: abs, MeasureTheory.tendsto_integral_filter_of_dominated_convergence
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

Tactic:
Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

Tactic:
exact Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_2 : ∀ (A : ℝ), ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a

Tactic:
filter_upwards with A
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
refine_2 : ∀ (x : α), ‖truncation f A x‖ ≤ |f x|
⊢ ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|

Tactic:
filter_upwards with x
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
abs_truncation_le_abs_self _ _ _

Premises used: ProbabilityTheory.abs_truncation_le_abs_self
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
exact abs_truncation_le_abs_self _ _ _

Premises used: ProbabilityTheory.abs_truncation_le_abs_self
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ |f x|) μ

Tactic:
hf.abs

Premises used: MeasureTheory.Integrable.abs
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ |f x|) μ

Tactic:
exact hf.abs

Premises used: MeasureTheory.Integrable.abs
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_4 : ∀ (x : α), Tendsto (fun (n : ℝ) ↦ truncation f n x) atTop (𝓝 (f x))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℝ) ↦ truncation f n a) atTop (𝓝 (f a))

Tactic:
filter_upwards with x
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
apply : EventuallyEq (β := ℝ) atTop (fun (x_1 : ℝ) ↦ f x) fun (n : ℝ) ↦ truncation f n x
⊢ Tendsto (fun (n : ℝ) ↦ truncation f n x) atTop (𝓝 (f x))

Tactic:
apply tendsto_const_nhds.congr' _

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
h : ∀ (A : ℝ) (hA : A ∈ Set.Ioi |f x|), f x = truncation f A x
⊢ EventuallyEq (β := ℝ) atTop (fun (x_1 : ℝ) ↦ f x) fun (n : ℝ) ↦ truncation f n x

Tactic:
filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA

Premises used: abs, Filter.Ioi_mem_atTop
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
hA : A ∈ Set.Ioi |f x|
⊢ f x = truncation f A x

Tactic:
(truncation_eq_self hA).symm

Premises used: ProbabilityTheory.truncation_eq_self, Eq.symm
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
hA : A ∈ Set.Ioi |f x|
⊢ f x = truncation f A x

Tactic:
exact (truncation_eq_self hA).symm

Premises used: ProbabilityTheory.truncation_eq_self, Eq.symm
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : MeasurableSpace β
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
A : ℝ
⊢ IdentDistrib (ProbabilityTheory.truncation f A) (ProbabilityTheory.truncation g A) μ ν

Tactic:
h.comp (measurable_id.indicator measurableSet_Ioc)

Premises used: measurable_id, Measurable.indicator, measurableSet_Ioc, ProbabilityTheory.IdentDistrib.comp, ProbabilityTheory.truncation
-- 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 ℙ
⊢ IsProbabilityMeasure ρ

Tactic:
haveI : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hint.aemeasurable
-- 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 ρ
apply :
  ∀ (j : ℕ) (hj : j ∈ range K),
    Eq (α := ℝ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ) (∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
    (∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)

Tactic:
apply 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 ρ
j : ℕ
hj : j ∈ range K
rw : ∀ k ∈ Set.Ico j N, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ) (∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]

Premises used: LT.lt.le, intervalIntegral.sum_integral_adjacent_intervals_Ico, Finset.mem_range, Iff.mp, 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 ρ
j : ℕ
hj : j ∈ range K
k : ℕ
_ : k ∈ Set.Ico j N → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ k ∈ Set.Ico j N → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
_
-- 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 : ℕ
hj : j ∈ range K
k : ℕ
h : k ∈ Set.Ico j N
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

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 ρ
j : ℕ
hj : j ∈ range K
k : ℕ
h : k ∈ Set.Ico j N
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

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 ρ
simp_rw :
  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 ∂ρ)
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
    (∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)

Tactic:
simp_rw [sum_sigma']

Premises used: Finset.sum_sigma'
-- 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 ρ
⊢ 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 ∂ρ)

Tactic:
sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Sigma.fst, Sigma.mk, Sigma.snd, Finset.sum_nbij'
-- 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 →
      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)

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 ρ
⊢ ∀ (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)

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 ρ
⊢ ∀ (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

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 ρ
⊢ ∀ (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:
aesop (add simp Nat.lt_succ_iff)

Premises used: Nat.lt_succ_iff