-- Mathlib/Probability/Kernel/Proper.lean
/-- Auxiliary lemma for `IsProper.lintegral_mul` and
`IsProper.setLIntegral_eq_indicator_mul_lintegral`. -/
private lemma IsProper.lintegral_indicator_mul (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧)
    (hf : Measurable[𝓧] f) (hB : MeasurableSet[𝓑] B) :
    ∫⁻ x, B.indicator 1 x * f x ∂(π x₀) = B.indicator 1 x₀ * ∫⁻ x, f x ∂(π x₀)

Proof state:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * f₁ x + B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x + f₂ x ∂π x₀

Tactic:
rw [lintegral_add_right, lintegral_add_right, hf₁, hf₂, mul_add] <;> measurability

Result:
no goals

Proof state:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
⊢ ∀ ⦃f g : X → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (x : X), B.indicator 1 x * f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀ →
            ∫⁻ (x : X), B.indicator 1 x * g x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), g x ∂π x₀ →
              ∫⁻ (x : X), B.indicator 1 x * (f + g) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), (f + g) x ∂π x₀

Tactic:
rintro f₁ f₂ - _ _ hf₁ hf₂

Result:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * (f₁ + f₂) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), (f₁ + f₂) x ∂π x₀

Proof state:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * (f₁ + f₂) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), (f₁ + f₂) x ∂π x₀

Tactic:
simp only [Pi.add_apply, mul_add]

Result:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * f₁ x + B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x + f₂ x ∂π x₀

Proof state:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), B.indicator 1 x * A.indicator (fun x => c) x ∂π x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator (fun x => c) x ∂π x₀

Tactic:
simp_rw [← smul_indicator_one_apply, mul_smul_comm, smul_eq_mul]

Result:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), c * (B.indicator 1 x * A.indicator 1 x) ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂π x₀

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ∀ (n : ℕ), Measurable fun x => B.indicator 1 x * f' n x

Tactic:
measurability

Result:
no goals

Proof state:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set X⦄,
    MeasurableSet s →
      ∫⁻ (x : X), B.indicator 1 x * s.indicator (fun x => c) x ∂π x₀ =
        B.indicator 1 x₀ * ∫⁻ (x : X), s.indicator (fun x => c) x ∂π x₀

Tactic:
rintro c A hA

Result:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), B.indicator 1 x * A.indicator (fun x => c) x ∂π x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator (fun x => c) x ∂π x₀