-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
refine_1 :
  ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
    (fun (ψ : SimpleFunc E E) ↦
        ∀ᵐ (ω : Ω) ∂μ,
          Tendsto.{0, u_2} (β := E)
            (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
            atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
      (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0))
refine_2 refine_2₁ :
  ∀ ⦃f g : SimpleFunc E E⦄,
    Disjoint (α := Set E) (Function.support (M := E) (⇑f : (a : E) → E))
        (Function.support (M := E) (⇑g : (a : E) → E)) →
      (fun (ψ : SimpleFunc E E) ↦
            ∀ᵐ (ω : Ω) ∂μ,
              Tendsto.{0, u_2} (β := E)
                (fun (n : ℕ) ↦
                  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
          f →
        (fun (ψ : SimpleFunc E E) ↦
              ∀ᵐ (ω : Ω) ∂μ,
                Tendsto.{0, u_2} (β := E)
                  (fun (n : ℕ) ↦
                    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                  atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
            g →
          (fun (ψ : SimpleFunc E E) ↦
              ∀ᵐ (ω : Ω) ∂μ,
                Tendsto.{0, u_2} (β := E)
                  (fun (n : ℕ) ↦
                    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
                  atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
            (f + g)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))

Tactic:
classical
  refine SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ
  · 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]
  · rintro φ ψ - hφ hψ
    filter_upwards [hφ, hψ] with ω hωφ hωψ
    convert! hωφ.add hωψ using 1
    · simp [sum_add_distrib]
    · congr 1
      rw [← integral_add]
      · rfl
      · exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure
      · exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Premises used: Finset.sum_smul, MeasureTheory.SimpleFunc.induction, Finset.sum_add_distrib, integral_smul_const, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, smul_smul, MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, Function.comp_apply, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, OfNat.ofNat, MeasureTheory.SimpleFunc.coe_const, MeasureTheory.integral_add, MeasureTheory.SimpleFunc.comp