-- Mathlib/Probability/StrongLaw.lean
theorem strong_law_ae_real {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    (X : ℕ → Ω → ℝ) (hint : Integrable (X 0) μ)
    (hindep : Pairwise ((IndepFun · · μ) on X))
    (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
    ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (∑ i ∈ range n, X i ω) / n) atTop (𝓝 μ[X 0])

Proof state:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (neg ∘ X i) ω) / n) atTop (𝓝 𝔼[neg ∘ X 0]) :=
  strong_law_aux7 _ hint.neg_part (fun i j hij => (hindep hij).comp negm negm)
    (fun i => (hident i).comp negm) fun i ω => le_max_right _ _

Result:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Proof state:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have posm : Measurable pos := measurable_id'.max measurable_const

Result:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Proof state:
case pos
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have I : ∀ᵐ ω, ∀ i, X i ω = 0 := by
  rw [ae_all_iff]
  intro i
  exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h

Result:
case pos
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Proof state:
case h
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
convert hωpos.sub hωneg using 2

Result:
case h.e'_3.h
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
x✝ : ℕ
⊢ (∑ i ∈ range x✝, X i ω) / ↑x✝ = (∑ i ∈ range x✝, (pos ∘ X i) ω) / ↑x✝ - (∑ i ∈ range x✝, (neg ∘ X i) ω) / ↑x✝

case h.e'_5.h.e'_3
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x => x ⊔ 0
neg : ℝ → ℝ := fun x => -x ⊔ 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n => (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n => (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ ∫ (x : Ω), X 0 x ∂μ = (∫ (a : Ω), (pos ∘ X 0) a) - ∫ (a : Ω), (neg ∘ X 0) a

Proof state:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have : IsProbabilityMeasure μ :=
  hint.isProbabilityMeasure_of_indepFun (X 0) (X 1) h (hindep zero_ne_one)

Result:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := MeasureSpace.mk μ
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))