awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
h_rnDeriv :
  ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ (i : Ω),
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i a =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) a
x : 𝓧
hx :
  (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
hx_all :
  ∀ (i : Ω),
    κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i x =
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
⊢ (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
have h : (μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x) =
  μ.withDensity fun (ω : Ω) ↦
    Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
Tactic: simp_rw [hx, hx_all]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π,
    ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {false} =
      HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞)
        ((∂μ/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
have h : ∀ (x : 𝓧)
  (hx :
    ((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x =
      π.withDensity fun (ω : Bool) ↦
        Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
          ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x),
  ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {false} =
    HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞)
      ((∂μ/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
Tactic: filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
x : 𝓧
hx :
  ((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x =
    π.withDensity fun (ω : Bool) ↦
      Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
        ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x
⊢ ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {false} =
    HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞)
      ((∂μ/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
have h : (π.withDensity fun (ω : Bool) ↦
        Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
          ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x :
      (a : Set Bool) → ℝ≥0∞)
    {false} =
  HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞)
    ((∂μ/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π,
    ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {true} =
      HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞)
        ((∂ν/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
have h : ∀ (x : 𝓧)
  (hx :
    ((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x =
      π.withDensity fun (ω : Bool) ↦
        Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
          ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x),
  ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {true} =
    HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞)
      ((∂ν/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
Tactic: filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
x : 𝓧
hx :
  ((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x =
    π.withDensity fun (ω : Bool) ↦
      Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
        ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x
⊢ ((((Kernel.boolKernel μ ν)†π : (a : 𝓧) → Measure Bool) x : Measure Bool) : (a : Set Bool) → ℝ≥0∞) {true} =
    HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞)
      ((∂ν/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
have h : (π.withDensity fun (ω : Bool) ↦
        Measure.rnDeriv (m := m𝓧) ((Kernel.boolKernel μ ν : (a : Bool) → Measure 𝓧) ω)
          ((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x :
      (a : Set Bool) → ℝ≥0∞)
    {true} =
  HMul.hMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞)
    ((∂ν/∂(⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure 𝓧) ∘ₘ π) x)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (π.restrict (s := B) ⋯ : (a : X) → Measure X) x =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
          ((π : (a : X) → Measure X) x : Measure X)
have refine_1 : π.IsProper →
  ∀
    (h :
      ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
        (π.restrict (s := B) sorry : (a : X) → Measure X) x =
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
            ((π : (a : X) → Measure X) x : Measure X))
    ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
    (π.restrict (s := B) sorry : (a : X) → Measure X) x =
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
        ((π : (a : X) → Measure X) x : Measure X)
Tactic: refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
refine_1 :
  π.IsProper →
    ∀
      (h :
        ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
          (π.restrict (s := B) ⋯ : (a : X) → Measure X) x =
            HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
              ((π : (a : X) → Measure X) x : Measure X))
      ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (π.restrict (s := B) ⋯ : (a : X) → Measure X) x =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
          ((π : (a : X) → Measure X) x : Measure X)
⊢ π.IsProper ↔
    ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (π.restrict (s := B) ⋯ : (a : X) → Measure X) x =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
          ((π : (a : X) → Measure X) x : Measure X)
have refine_2 : ∀
  (h :
    ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (π.restrict (s := B) sorry : (a : X) → Measure X) x =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x)
          ((π : (a : X) → Measure X) x : Measure X))
  ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
  (π.restrict (s := B) sorry : (a : X) → Measure X) x =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure X) (B.indicator (fun (x : X) ↦ 1) x) ((π : (a : X) → Measure X) x : Measure X)
Tactic: refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (((π.restrict (s := B) ⋯ : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have simp : (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
    MeasurableSet s →
      (((π.restrict (s := B) sorry : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) s =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator (fun (x : X) ↦ 1) x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)) ↔
  ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
    (((π.restrict (s := B) sorry : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (((π.restrict (s := B) ⋯ : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (_hB : MeasurableSet B) (x : X),
      (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have a : ∀ (A : Set X) (hA : MeasurableSet A) (B : Set X) (hB : MeasurableSet B) (x : X),
  (((π.restrict (s := B) sorry : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
    (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: congr! 5 with A hA B hB x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ (((π.restrict (s := B) ⋯ : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
    (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have a : ((Measure.restrict ((π : (a : X) → Measure X) x) B : Measure X) : (a : Set X) → ℝ≥0∞) A =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
      ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
  (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
      ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [restrict_apply, Measure.restrict_apply hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
a :
  ((Measure.restrict ((π : (a : X) → Measure X) x) B : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
    (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
⊢ (((π.restrict (s := B) ⋯ : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
    (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have a₁ : (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
      ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞) ↔
  (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
      ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [restrict_apply, Measure.restrict_apply hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (_hB : MeasurableSet B) (x : X),
      (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have _ : π.IsProper ↔
  ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
    (((π.restrict (s := B) sorry : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: calc
    _ ↔ ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
          π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A := by
      simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
    _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
_ :
  π.IsProper ↔
    ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
      (((π.restrict (s := B) ⋯ : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (_hB : MeasurableSet B) (x : X),
      (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
          ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
have _₁ : (∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X),
    (((π.restrict (s := B) sorry : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)) ↔
  ∀ ⦃A : Set X⦄ (_hA : MeasurableSet A) ⦃B : Set X⦄ (_hB : MeasurableSet B) (x : X),
    (((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (B.indicator 1 x : ℝ≥0∞)
        ((((π : (a : X) → Measure X) x : Measure X) : (a : Set X) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: calc
    _ ↔ ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
          π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A := by
      simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
    _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A ∂μ =
    (((⇑π : (a : X) → Measure X) ∘ₘ μ : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B)
have rw : ∫⁻ (a : X) in B, (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A ∂μ =
  ∫⁻ (a : X), (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) ∂μ
Tactic: rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A ∂μ =
    ∫⁻ (a : X), (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) (A ∩ B) ∂μ
have simp : ∫⁻ (a : X) in B, (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A ∂μ =
  ∫⁻ (a : X), B.indicator (fun (x : X) ↦ (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A) a ∂μ
Tactic: simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A ∂μ =
    ∫⁻ (a : X), B.indicator (fun (x : X) ↦ (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A) a ∂μ
have rw : ∫⁻ (a : X), B.indicator (fun (a : X) ↦ (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A) a ∂μ =
  ∫⁻ (a : X), B.indicator (fun (x : X) ↦ (((π : (a : X) → Measure X) a : Measure X) : (a : Set X) → ℝ≥0∞) A) a ∂μ
Tactic: rw [← lintegral_indicator (h𝓑𝓧 _ hB)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (x : X), HMul.hMul (α := ℝ≥0∞) (B.indicator 1 x) (A.indicator 1 x) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂(π : (a : X) → Measure X) x₀
have simp_rw : ∫⁻ (x : X), (B ∩ A).indicator (fun (j : X) ↦ HMul.hMul (α := ℝ≥0∞) (1 j) (1 j)) x ∂(π : (a : X) → Measure X) x₀ =
  B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂(π : (a : X) → Measure X) x₀
Tactic: simp_rw [← inter_indicator_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (x : X), (B ∩ A).indicator (fun (j : X) ↦ HMul.hMul (α := ℝ≥0∞) (1 j) (1 j)) x ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂(π : (a : X) → Measure X) x₀
have rw : ∫⁻ (a : X) in B ∩ A, HMul.hMul (α := ℝ≥0∞) (1 a) (1 a) ∂(π : (a : X) → Measure X) x₀ =
  B.indicator 1 x₀ * ∫⁻ (a : X) in A, 1 a ∂(π : (a : X) → Measure X) x₀
Tactic: rw [lintegral_indicator ((h𝓑𝓧 _ hB).inter hA), lintegral_indicator hA]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ ∫⁻ (a : X) in B ∩ A, HMul.hMul (α := ℝ≥0∞) (1 a) (1 a) ∂(π : (a : X) → Measure X) x₀ =
    B.indicator 1 x₀ * ∫⁻ (a : X) in A, 1 a ∂(π : (a : X) → Measure X) x₀
have simp : (((π : (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: simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
    Pi.one_apply, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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
⊢ (((π : (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∞)
have 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∞)
Tactic: rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Proper (goal)
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∞)
⊢ (((π : (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∞)
have 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∞)
Tactic: rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_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
⊢ ∫⁻ (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_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₀
Tactic: refine hf.ennreal_induction ?_ ?_ ?_