-- Mathlib/Probability/StrongLaw.lean
/-- Preliminary lemma for the strong law of large numbers for vector-valued random variables,
assuming measurability in addition to integrability. This is weakened to ae measurability in
the full version `ProbabilityTheory.strong_law_ae`. -/
lemma strong_law_ae_of_measurable
    (X : ℕ → Ω → E) (hint : Integrable (X 0) μ) (h' : StronglyMeasurable (X 0))
    (hindep : Pairwise ((IndepFun · · μ) on X))
    (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
    ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ ↦ (n : ℝ) ⁻¹ • (∑ i ∈ range n, X i ω)) atTop (𝓝 μ[X 0])

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i => ⇑(φ k) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω)‖ +
        ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ +
      ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ ≤
    (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / ↑n + δ + δ

Tactic:
gcongr

Result:
case h₁.h₁
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i => ⇑(φ k) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω => ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n => (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
J : ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
n : ℕ
hn : (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
h'n : ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
⊢ ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, (X i ω - Y k i ω)‖ ≤ (∑ i ∈ Finset.range n, ‖X i ω - Y k i ω‖) / ↑n

Proof state:
case hident
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i => ⇑(φ k) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x => ‖x - (φ k) x‖
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω => ‖(X i - Y k i) ω‖) = G k ∘ X i
i : ℕ
⊢ IdentDistrib (fun ω => ‖(X i - Y k i) ω‖) (fun ω => ‖(X 0 - Y k 0) ω‖) μ μ

Tactic:
simp_rw [I]

Result:
case hident
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k => Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i => ⇑(φ k) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x => ‖x - (φ k) x‖
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω => ‖(X i - Y k i) ω‖) = G k ∘ X i
i : ℕ
⊢ IdentDistrib (G k ∘ X i) (G k ∘ X 0) μ μ