-- Mathlib/Probability/Kernel/Proper.lean
lemma IsProper.lintegral_mul (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable[𝓧] f)
    (hg : Measurable[𝓑] g) (x₀ : X) :
    ∫⁻ x, g x * f x ∂(π x₀) = g x₀ * ∫⁻ x, f x ∂(π x₀)

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

Tactic:
rintro g₁ g₂ - _ hg₂_meas hg₁ hg₂

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

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

Tactic:
simp only [Pi.add_apply, mul_add, add_mul]

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

Proof state:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ∫⁻ (x : X), ⨆ i, g' i x * f x ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
rw [lintegral_iSup (fun n ↦ ((hg'_meas _).mono h𝓑𝓧 le_rfl).mul hf)
  (hg'_mono.mul_const (zero_le _))]

Result:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), g' n a * f a ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀

Proof state:
case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x => A.indicator 1 x * f x

Tactic:
measurability

Result:
no goals

Proof state:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∀ ⦃f_1 : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (x : X), f_1 n x * f x ∂π x₀ = f_1 n x₀ * ∫⁻ (x : X), f x ∂π x₀) →
          ∫⁻ (x : X), (fun x => ⨆ n, f_1 n x) x * f x ∂π x₀ = (fun x => ⨆ n, f_1 n x) x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
rintro g' hg'_meas hg'_mono hg'

Result:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ∫⁻ (x : X), (fun x => ⨆ n, g' n x) x * f x ∂π x₀ = (fun x => ⨆ n, g' n x) x₀ * ∫⁻ (x : X), f x ∂π x₀

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

Tactic:
rw [lintegral_add_right, hg₁, hg₂]

Result:
case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x => g₂ x * f x

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

Tactic:
rintro c A hA

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

Proof state:
case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x => g₂ x * f x

Tactic:
exact (hg₂_meas.mono h𝓑𝓧 le_rfl).mul hf

Result:
no goals

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
refine hg.ennreal_induction ?_ ?_ ?_

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

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

case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
⊢ ∀ ⦃f_1 : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (x : X), f_1 n x * f x ∂π x₀ = f_1 n x₀ * ∫⁻ (x : X), f x ∂π x₀) →
          ∫⁻ (x : X), (fun x => ⨆ n, f_1 n x) x * f x ∂π x₀ = (fun x => ⨆ n, f_1 n x) x₀ * ∫⁻ (x : X), f x ∂π x₀