Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: 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 ↦ 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)⁻¹ •
            ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
        atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))

pp: case refine_2
Ω : 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 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
⊢ ∀ ⦃f g : SimpleFunc E E⦄,
    Disjoint (Function.support ⇑f) (Function.support ⇑g) →
      (∀ᵐ (ω : Ω) ∂μ,
          Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, f (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑f ∘ X 0) x ∂μ))) →
        (∀ᵐ (ω : Ω) ∂μ,
            Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, g (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑g ∘ X 0) x ∂μ))) →
          ∀ᵐ (ω : Ω) ∂μ,
            Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, (f + g) (X i ω)) atTop
              (𝓝 (∫ (x : Ω), (⇑(f + g) ∘ X 0) x ∂μ))

Tactic:
· intro c s hs
    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, piecewise_eq_indicator, Function.comp_apply]
    let F : E → ℝ := indicator s 1
    have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs
    let Y : ℕ → Ω → ℝ := fun n ↦ F ∘ (X n)
    have : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ (n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y i ω)
        atTop (𝓝 μ[Y 0]) := by
      simp only [smul_eq_mul, ← div_eq_inv_mul]
      apply strong_law_ae_real
      · exact SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')
      · exact fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas
      · exact fun i ↦ (hident i).comp F_meas
    filter_upwards [this] with ω hω
    have I : indicator s (Function.const E c) = (fun x ↦ (indicator s (1 : E → ℝ) x) • c) := by
      ext
      rw [← indicator_smul_const_apply]
      congr! 1
      ext
      simp
    simp only [I, integral_smul_const]
    convert! Tendsto.smul_const hω c using 1
    simp [F, Y, ← sum_smul, smul_smul]

Goal state after:
case refine_2
Ω : 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 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
⊢ ∀ ⦃f g : SimpleFunc E E⦄,
    Disjoint (Function.support ⇑f) (Function.support ⇑g) →
      (∀ᵐ (ω : Ω) ∂μ,
          Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, f (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑f ∘ X 0) x ∂μ))) →
        (∀ᵐ (ω : Ω) ∂μ,
            Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, g (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑g ∘ X 0) x ∂μ))) →
          ∀ᵐ (ω : Ω) ∂μ,
            Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, (f + g) (X i ω)) atTop
              (𝓝 (∫ (x : Ω), (⇑(f + g) ∘ X 0) x ∂μ))