awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀
Tactic: refine hf.ennreal_induction ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀
Tactic: refine hf.ennreal_induction ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (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₀
have 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₀
Tactic: simp_rw [← smul_indicator_one_apply, mul_smul_comm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (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₀
have refine_1 : Measurable (β := ℝ≥0∞) (A.indicator 1)
Tactic: rw [lintegral_const_mul, lintegral_const_mul, hπ.lintegral_indicator_mul_indicator h𝓑𝓧 hA hB,
      mul_left_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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)
⊢ ∫⁻ (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₀
have refine_1₁ : Measurable (β := ℝ≥0∞) fun (x : X) ↦ HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x)
Tactic: rw [lintegral_const_mul, lintegral_const_mul, hπ.lintegral_indicator_mul_indicator h𝓑𝓧 hA hB,
      mul_left_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀
Tactic: simp only [Pi.add_apply, mul_add]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₂
⊢ ∫⁻ (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₀
have refine_2₁ : Measurable (β := ℝ≥0∞) fun (x : X) ↦ B.indicator 1 x * f₂ x
Tactic: rw [lintegral_add_right, lintegral_add_right, hf₁, hf₂, mul_add]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀
Tactic: simp_rw [ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀)
Tactic: rw [lintegral_iSup (by measurability), lintegral_iSup hf'_meas hf'_mono, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀)
⊢ ∫⁻ (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₀
have refine_3₁ : Monotone.{0, u_1} (β := X → ℝ≥0∞) fun (i : ℕ) (x : X) ↦ B.indicator 1 x * f' i x
Tactic: rw [lintegral_iSup (by measurability), lintegral_iSup hf'_meas hf'_mono, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (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₀
have rw : Measurable (A.indicator f)
Tactic: rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB,
    setLIntegral_indicator]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
have 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₀
Tactic: refine hg.ennreal_induction ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (x : X), g x * f x ∂(π : (a : X) → Measure X) x₀ = g x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
have 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₀
Tactic: refine hg.ennreal_induction ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (x : X), g x * f x ∂(π : (a : X) → Measure X) x₀ = g x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
have 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₀
Tactic: refine hg.ennreal_induction ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (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₀
have 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₀)
Tactic: simp_rw [← smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (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₀)
have refine_1 : Measurable (β := ℝ≥0∞) fun (x : X) ↦ A.indicator 1 x * f x
Tactic: rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (x : X), (g₁ + g₂) x * f x ∂(π : (a : X) → Measure X) x₀ =
    (g₁ + g₂) x₀ * ∫⁻ (x : X), f x ∂(π : (a : X) → Measure X) x₀
have 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₀
Tactic: simp only [Pi.add_apply, add_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have refine_2 : Measurable (β := ℝ≥0∞) fun (x : X) ↦ g₂ x * f x
Tactic: rw [lintegral_add_right, hg₁, hg₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀
Tactic: simp_rw [ENNReal.iSup_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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₀
⊢ ∫⁻ (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₀
have 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₀)
Tactic: rw [lintegral_iSup (fun n ↦ ((hg'_meas _).mono h𝓑𝓧 le_rfl).mul hf)
      (hg'_mono.mul_const zero_le)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ LE.le (α := ℝ) 0
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)
have pos : ∀ (hα : Countable α),
  0 ≤ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
pos :
  ∀ (hα : Countable α),
    0 ≤ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
⊢ LE.le (α := ℝ) 0
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)
have neg : ∀ (hα : ¬Countable α),
  0 ≤ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
⊢ 0 ≤ density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ
have this : MeasurableSpace.CountablyGenerated γ
Tactic: have := hαγ.countableOrCountablyGenerated.resolve_left hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
⊢ κ.rnDerivAux η a ≤ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)] 1
have h : ∀ (x : γ) (hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x),
  κ.rnDerivAux η a x ≤ 1 x
Tactic: filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
⊢ LE.le (α := ℝ)
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)
    (1 x)
have pos : ∀ (hα : Countable α),
  (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
pos :
  ∀ (hα : Countable α),
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x
⊢ LE.le (α := ℝ)
    (if hα : Countable α then
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal
    else density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ)
    (1 x)
have neg : ∀ (hα : ¬Countable α),
  density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) η a x univ ≤ 1 x
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
⊢ (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x).toReal ≤ 1 x
have pos : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ ENNReal.ofReal (1 x)
Tactic: refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1 x
hα : Countable α
⊢ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ ENNReal.ofReal (1 x)
have pos : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≤ 1
Tactic: simp only [Pi.one_apply, ENNReal.ofReal_one]