awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
rw :
  Eq (α := ℝ≥0∞) ((((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) (B ∩ A) : ℝ≥0∞)
    ((((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) : ℝ≥0∞)
    ((((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) : ℝ≥0∞)
⊢ (((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) (B ∩ A) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x₀ : ℝ≥0∞)
      ((((π : (a : X) → Measure X) x₀ : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_comm]

Premises used: Set.inter_comm, ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
⊢ ∫⁻ (x : X), B.indicator 1 x * f x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
hf.ennreal_induction ?_ ?_ ?_

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
refine_1 :
  ∀ (c : ℝ≥0∞) ⦃s : Set X⦄,
    MeasurableSet s →
      ∫⁻ (x : X),
          HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (s.indicator (fun (x : X) ↦ c) x) ∂(π : (a : X) → Measure X) x₀ =
        B.indicator 1 x₀ * ∫⁻ (x : X), s.indicator (fun (x : X) ↦ c) x ∂(π : (a : X) → Measure X) x₀
refine_2 :
  ∀ ⦃f g : X → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (x : X), B.indicator 1 x * f x ∂(π : (a : X) → Measure X) x₀ =
              B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀ →
            ∫⁻ (x : X), B.indicator 1 x * g x ∂(π : (a : X) → Measure X) x₀ =
                B.indicator 1 x₀ * ∫⁻ (x : X), g x ∂(π : (a : X) → Measure X) x₀ →
              ∫⁻ (x : X), B.indicator 1 x * (f + g) x ∂(π : (a : X) → Measure X) x₀ =
                B.indicator 1 x₀ * ∫⁻ (x : X), (f + g) x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  ∀ ⦃f : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (x : X), B.indicator 1 x * f n x ∂(π : (a : X) → Measure X) x₀ =
              B.indicator 1 x₀ * ∫⁻ (x : X), f n x ∂(π : (a : X) → Measure X) x₀) →
          ∫⁻ (x : X),
              HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x)
                ((fun (x : X) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) x) ∂(π : (a : X) → Measure X) x₀ =
            B.indicator 1 x₀ * ∫⁻ (x : X), (fun (x : X) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * f x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
refine hf.ennreal_induction ?_ ?_ ?_
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
refine_1 :
  ∫⁻ (x : X), c * HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator (fun (x : X) ↦ c) x) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator (fun (x : X) ↦ c) x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp_rw [← smul_indicator_one_apply, mul_smul_comm, smul_eq_mul]

Premises used: Set.smul_indicator_one_apply, mul_smul_comm, smul_eq_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
refine_1 : Measurable (β := ℝ≥0∞) (A.indicator 1)
refine_1₁ : Measurable (β := ℝ≥0∞) fun (x : X) ↦ HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x)
⊢ ∫⁻ (x : X), c * HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), c * A.indicator 1 x ∂(π : (a : X) → Measure X) x₀

Tactic:
rw [lintegral_const_mul, lintegral_const_mul, hπ.lintegral_indicator_mul_indicator h𝓑𝓧 hA hB,
      mul_left_comm]

Premises used: mul_left_comm, _private.0.ProbabilityTheory.Kernel.IsProper.lintegral_indicator_mul_indicator, MeasureTheory.lintegral_const_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
⊢ Measurable (β := ℝ≥0∞) (A.indicator 1)

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
⊢ Measurable (β := ℝ≥0∞) fun (x : X) ↦ HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x)

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable f₁
h_1 : Measurable f₂
hf₁ :
  ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂(π : (a : X) → Measure X) x₀
hf₂ :
  ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂(π : (a : X) → Measure X) x₀
refine_2 :
  ∫⁻ (x : X), B.indicator 1 x * f₁ x + B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x + f₂ x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * (f₁ + f₂) x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), (f₁ + f₂) x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp only [Pi.add_apply, mul_add]

Premises used: Pi.add_apply, mul_add
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable f₁
h_1 : Measurable f₂
hf₁ :
  ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂(π : (a : X) → Measure X) x₀
hf₂ :
  ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂(π : (a : X) → Measure X) x₀
refine_2 : Measurable f₂
refine_2₁ : Measurable (β := ℝ≥0∞) fun (x : X) ↦ B.indicator 1 x * f₂ x
⊢ ∫⁻ (x : X), B.indicator 1 x * f₁ x + B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x + f₂ x ∂(π : (a : X) → Measure X) x₀

Tactic:
rw [lintegral_add_right, lintegral_add_right, hf₁, hf₂, mul_add]

Premises used: mul_add, MeasureTheory.lintegral_add_right
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable f₁
h_1 : Measurable f₂
hf₁ :
  ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂(π : (a : X) → Measure X) x₀
hf₂ :
  ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂(π : (a : X) → Measure X) x₀
⊢ Measurable f₂

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable f₁
h_1 : Measurable f₂
hf₁ :
  ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂(π : (a : X) → Measure X) x₀
hf₂ :
  ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂(π : (a : X) → Measure X) x₀
⊢ Measurable (β := ℝ≥0∞) fun (x : X) ↦ B.indicator 1 x * f₂ x

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  ∫⁻ (x : X), ⨆ (i : ℕ), B.indicator 1 x * f' i x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), ⨆ (n : ℕ), f' n x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X),
      HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x)
        ((fun (x : X) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) x) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), (fun (x : X) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp_rw [ENNReal.mul_iSup]

Premises used: ENNReal.mul_iSup
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (x : X) ↦ B.indicator 1 x * f' n x

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : X), B.indicator 1 a * f' n a ∂(π : (a : X) → Measure X) x₀)
    (⨆ (i : ℕ), B.indicator 1 x₀ * ∫⁻ (a : X), f' i a ∂(π : (a : X) → Measure X) x₀)
refine_3₁ : Monotone.{0, u_1} (β := X → ℝ≥0∞) fun (i : ℕ) (x : X) ↦ B.indicator 1 x * f' i x
⊢ ∫⁻ (x : X), ⨆ (i : ℕ), B.indicator 1 x * f' i x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), ⨆ (n : ℕ), f' n x ∂(π : (a : X) → Measure X) x₀

Tactic:
rw [lintegral_iSup (by measurability), lintegral_iSup hf'_meas hf'_mono, ENNReal.mul_iSup]

Premises used: MeasureTheory.lintegral_iSup, ENNReal.mul_iSup
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : X), B.indicator 1 a * f' n a ∂(π : (a : X) → Measure X) x₀)
    (⨆ (i : ℕ), B.indicator 1 x₀ * ∫⁻ (a : X), f' i a ∂(π : (a : X) → Measure X) x₀)

Tactic:
simp_rw [hf']
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
⊢ Monotone.{0, u_1} (β := X → ℝ≥0∞) fun (i : ℕ) (x : X) ↦ B.indicator 1 x * f' i x

Tactic:
hf'_mono.const_mul zero_le

Premises used: zero_le, Monotone.const_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ =
      B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂(π : (a : X) → Measure X) x₀
⊢ Monotone.{0, u_1} (β := X → ℝ≥0∞) fun (i : ℕ) (x : X) ↦ B.indicator 1 x * f' i x

Tactic:
exact hf'_mono.const_mul zero_le

Premises used: zero_le, Monotone.const_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
x₀ : X
⊢ ∫⁻ (x : X) in B, f x ∂(π : (a : X) → Measure X) x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp [← hπ.lintegral_indicator_mul h𝓑𝓧 hf hB, ← indicator_mul_left,
    lintegral_indicator (h𝓑𝓧 _ hB)]

Premises used: _private.0.ProbabilityTheory.Kernel.IsProper.lintegral_indicator_mul, MeasureTheory.lintegral_indicator, Set.indicator_mul_left
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
hs : MeasurableSet A
rw : Measurable (A.indicator f)
⊢ ∫⁻ (x : X) in A ∩ B, f x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂(π : (a : X) → Measure X) x₀

Tactic:
rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB,
    setLIntegral_indicator]

Premises used: MeasureTheory.lintegral_indicator, ProbabilityTheory.Kernel.IsProper.setLIntegral_eq_indicator_mul_lintegral, MeasureTheory.setLIntegral_indicator
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ MeasurableSet A

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ Measurable (A.indicator f)

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ = g x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
hg.ennreal_induction ?_ ?_ ?_

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
refine_1 :
  ∀ (c : ℝ≥0∞) ⦃s : Set X⦄,
    MeasurableSet s →
      ∫⁻ (x : X), s.indicator (fun (x : X) ↦ c) x * f x ∂(π : (a : X) → Measure X) x₀ =
        s.indicator (fun (x : X) ↦ c) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_2 :
  ∀ ⦃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 ∂(π : (a : X) → Measure X) x₀ =
              f_1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀ →
            ∫⁻ (x : X), g x * f x ∂(π : (a : X) → Measure X) x₀ = g x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀ →
              ∫⁻ (x : X), (f_1 + g) x * f x ∂(π : (a : X) → Measure X) x₀ =
                (f_1 + g) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  ∀ ⦃f_1 : ℕ → X → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ),
            ∫⁻ (x : X), f_1 n x * f x ∂(π : (a : X) → Measure X) x₀ =
              f_1 n x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀) →
          ∫⁻ (x : X), (fun (x : X) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) x * f x ∂(π : (a : X) → Measure X) x₀ =
            (fun (x : X) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), g x * f x ∂(π : (a : X) → Measure X) x₀ = g x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
refine hg.ennreal_induction ?_ ?_ ?_
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
refine_1 :
  ∫⁻ (x : X), c * (A.indicator 1 x * f x) ∂(π : (a : X) → Measure X) x₀ =
    c * (A.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀)
⊢ ∫⁻ (x : X), A.indicator (fun (x : X) ↦ c) x * f x ∂(π : (a : X) → Measure X) x₀ =
    A.indicator (fun (x : X) ↦ c) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp_rw [← smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul]

Premises used: Set.smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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
refine_1 : Measurable (β := ℝ≥0∞) fun (x : X) ↦ A.indicator 1 x * f x
⊢ ∫⁻ (x : X), c * (A.indicator 1 x * f x) ∂(π : (a : X) → Measure X) x₀ =
    c * (A.indicator 1 x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀)

Tactic:
rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]

Premises used: _private.0.ProbabilityTheory.Kernel.IsProper.lintegral_indicator_mul, MeasureTheory.lintegral_const_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 (β := ℝ≥0∞) fun (x : X) ↦ A.indicator 1 x * f x

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂(π : (a : X) → Measure X) x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂(π : (a : X) → Measure X) x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_2 :
  ∫⁻ (x : X), g₁ x * f x + g₂ x * f x ∂(π : (a : X) → Measure X) x₀ =
    g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), (g₁ + g₂) x * f x ∂(π : (a : X) → Measure X) x₀ =
    (g₁ + g₂) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp only [Pi.add_apply, add_mul]

Premises used: add_mul, Pi.add_apply
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂(π : (a : X) → Measure X) x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂(π : (a : X) → Measure X) x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_2 : Measurable (β := ℝ≥0∞) fun (x : X) ↦ g₂ x * f x
⊢ ∫⁻ (x : X), g₁ x * f x + g₂ x * f x ∂(π : (a : X) → Measure X) x₀ =
    g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

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

Premises used: MeasureTheory.lintegral_add_right
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂(π : (a : X) → Measure X) x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂(π : (a : X) → Measure X) x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ Measurable (β := ℝ≥0∞) fun (x : X) ↦ g₂ x * f x

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

Premises used: Measurable.mul, le_rfl, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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∞
h : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂(π : (a : X) → Measure X) x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂(π : (a : X) → Measure X) x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ Measurable (β := ℝ≥0∞) fun (x : X) ↦ g₂ x * f x

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

Premises used: Measurable.mul, le_rfl, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  ∫⁻ (x : X), ⨆ (i : ℕ), g' i x * f x ∂(π : (a : X) → Measure X) x₀ =
    ⨆ (i : ℕ), g' i x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ ∫⁻ (x : X), (fun (x : X) ↦ (⨆ (n : ℕ), g' n x : ℝ≥0∞)) x * f x ∂(π : (a : X) → Measure X) x₀ =
    (fun (x : X) ↦ (⨆ (n : ℕ), g' n x : ℝ≥0∞)) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

Tactic:
simp_rw [ENNReal.iSup_mul]

Premises used: ENNReal.iSup_mul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
refine_3 :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : X), g' n a * f a ∂(π : (a : X) → Measure X) x₀)
    (⨆ (i : ℕ), g' i x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀)
⊢ ∫⁻ (x : X), ⨆ (i : ℕ), g' i x * f x ∂(π : (a : X) → Measure X) x₀ =
    ⨆ (i : ℕ), g' i x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀

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

Premises used: zero_le, Measurable.mul, le_rfl, Monotone.mul_const, MeasureTheory.lintegral_iSup, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
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 ∂(π : (a : X) → Measure X) x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : X), g' n a * f a ∂(π : (a : X) → Measure X) x₀)
    (⨆ (i : ℕ), g' i x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀)

Tactic:
simp_rw [hg']