-- Mathlib/Probability/StrongLaw.lean
/-- Preliminary lemma for the strong law of large numbers for vector-valued random variables:
the composition of the random variables with a simple function satisfies the strong law of large
numbers. -/
lemma strong_law_ae_simpleFunc_comp (X : ℕ → Ω → E) (h' : Measurable (X 0))
    (hindep : Pairwise ((IndepFun · · μ) on X))
    (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) (φ : SimpleFunc E E) :
    ∀ᵐ ω ∂μ,
      Tendsto (fun n : ℕ ↦ (n : ℝ) ⁻¹ • (∑ i ∈ range n, φ (X i ω))) atTop (𝓝 μ[φ ∘ (X 0)])

Proof state:
case h.e'_5.e_x
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ ∫ (x : Ω), (⇑(φ + ψ) ∘ X 0) x ∂μ = ∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ + ∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ

Tactic:
rw [← integral_add]

Result:
case h.e'_5.e_x
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ ∫ (x : Ω), (⇑(φ + ψ) ∘ X 0) x ∂μ = ∫ (a : Ω), (⇑φ ∘ X 0) a + (⇑ψ ∘ X 0) a ∂μ

case h.e'_5.e_x.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ Integrable (⇑φ ∘ X 0) μ

case h.e'_5.e_x.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ Integrable (⇑ψ ∘ X 0) μ

Proof state:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
let F : E → ℝ := indicator s 1

Result:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n => (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator (Function.const E c) (X x ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Proof state:
case h.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 => IndepFun x1 x2 μ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n => F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun x => s.indicator 1 x • c
⊢ (fun n => (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator 1 (X x ω) • c) = fun x =>
    ((↑x)⁻¹ • ∑ i ∈ Finset.range x, Y i ω) • c

Tactic:
simp [F, Y, ← sum_smul, smul_smul]

Result:
no goals