Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨a.snd, a.fst⟩ ∈ (range N).sigma fun a ↦ range (min (a + 1) K)

pp: case refine_2
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨a.snd, a.fst⟩ ∈ (range K).sigma fun a ↦ Ico a N

pp: case refine_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

pp: case refine_4
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

pp: case refine_5
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N,
    ∫ (x : ℝ) in ↑a.snd..↑(a.snd + 1), 1 ∂ρ = ∫ (x : ℝ) in ↑⟨a.snd, a.fst⟩.fst..↑(⟨a.snd, a.fst⟩.fst + 1), 1 ∂ρ

Tactic:
<;>

Goal state after:
case refine_1
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨a.snd, a.fst⟩ ∈ (range N).sigma fun a ↦ range (min (a + 1) K)

case refine_2
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨a.snd, a.fst⟩ ∈ (range K).sigma fun a ↦ Ico a N

case refine_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_4
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range N).sigma fun a ↦ range (min (a + 1) K), ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case refine_5
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∀ a ∈ (range K).sigma fun a ↦ Ico a N,
    ∫ (x : ℝ) in ↑a.snd..↑(a.snd + 1), 1 ∂ρ = ∫ (x : ℝ) in ↑⟨a.snd, a.fst⟩.fst..↑(⟨a.snd, a.fst⟩.fst + 1), 1 ∂ρ