-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
rw :
  HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)
          (∫ (a : Ω), ∏ x : S, (g x : (a : E x) → ℝ) (X x a) ∂P : ℝ) -
      HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
    (HSMul.hSMul (β := ℝ) ((P.restrict A).real Set.univ) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
        HSMul.hSMul (β := ℝ) ((P.restrict Aᶜ).real Set.univ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
      ∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P
hf : Integrable (ε := ℝ) (A.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) P
hg₁ : Integrable (ε := ℝ) (Aᶜ.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) P
⊢ ∫ (x : Ω),
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            x +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          x ∂P =
    HMul.hMul (α := ℝ)
      (∫ (x : Ω),
        HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) x)
          (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) x) ∂P)
      (∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P)
have hf₁ : Integrable (ε := ℝ)
  (A.indicator fun (ω : Ω) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
  P
Tactic: rw [integral_sub, integral_add, integral_indicator₀ mA, integral_indicator₀ mA,
    integral_const_mul, integral_const_mul, integral_const_mul, integral_add,
    integral_indicator₀ mA, integral_indicator₀ mA.compl, integral_const, integral_const, h]