awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Posterior
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
h :
  (μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x) =
    μ.withDensity fun (ω : Ω) ↦
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
⊢ (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x

Tactic:
simp_rw [hx, hx_all]
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
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)
⊢ ∀ᵐ (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)

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx

Premises used: ProbabilityTheory.Kernel.boolKernel, ProbabilityTheory.posterior_eq_withDensity_of_countable
-- Module: Mathlib.Probability.Kernel.Posterior
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
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)
⊢ ((((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:
rw [hx]
-- Module: Mathlib.Probability.Kernel.Posterior
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
⊢ (π.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:
simp
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
π : Measure Bool
inst_2 : IsFiniteMeasure π
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)
⊢ ∀ᵐ (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)

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx

Premises used: ProbabilityTheory.Kernel.boolKernel, ProbabilityTheory.posterior_eq_withDensity_of_countable
-- Module: Mathlib.Probability.Kernel.Posterior
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
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)
⊢ ((((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:
rw [hx]
-- Module: Mathlib.Probability.Kernel.Posterior
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
⊢ (π.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:
simp
-- Module: Mathlib.Probability.Kernel.Proper
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)

Tactic:
⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩

Premises used: Iff.intro, ProbabilityTheory.Kernel.IsProper.mk, _private.0.ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul.match_1
-- Module: Mathlib.Probability.Kernel.Proper
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)
refine_2 :
  ∀
    (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)

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
h_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)

Tactic:
simpa +instances only [inf_eq_left.2 h𝓑𝓧] using h

Premises used: Iff.mpr, inf_eq_left
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
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)

Tactic:
simpa +instances only [inf_eq_left.2 h𝓑𝓧] using h

Premises used: Iff.mpr, inf_eq_left
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
simp :
  (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s →
        (((π.restrict (s := B) ⋯ : (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) ⋯ : (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),
      (((π.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∞)

Tactic:
simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]

Premises used: MeasureTheory.Measure.ext_iff, ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s →
        (((π.restrict (s := B) ⋯ : (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) ⋯ : (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:
aesop
-- Module: Mathlib.Probability.Kernel.Proper
Goal:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
a :
  ∀ (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∞)
⊢ (∀ ⦃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∞)

Tactic:
congr! 5 with A hA B hB x
-- Module: Mathlib.Probability.Kernel.Proper
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∞)
a₁ 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∞)
⊢ (((π.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∞)

Tactic:
rw [restrict_apply, Measure.restrict_apply hA]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.Probability.Kernel.Proper
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∞)
_₁ :
  (∀ ⦃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∞)
⊢ π.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∞)

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]
-- Module: Mathlib.Probability.Kernel.Proper
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
⊢ MeasurableSet (A ∩ B)

Tactic:
measurability
-- Module: Mathlib.Probability.Kernel.Proper
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
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) ∂μ
⊢ ∫⁻ (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)

Tactic:
rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]

Premises used: MeasureTheory.Measure.bind_apply, le_rfl, Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable, Measurable.mono
-- Module: Mathlib.Probability.Kernel.Proper
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
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 ∂μ
⊢ ∫⁻ (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:
simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]

Premises used: Pi.one_apply, Set.indicator_mul_const, one_mul, ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul
-- Module: Mathlib.Probability.Kernel.Proper
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
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 ∂μ
⊢ ∫⁻ (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:
rw [← lintegral_indicator (h𝓑𝓧 _ hB)]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.Probability.Kernel.Proper
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), 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:
rfl
-- 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
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₀
⊢ ∫⁻ (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₀

Tactic:
simp_rw [← inter_indicator_mul]

Premises used: Set.inter_indicator_mul
-- 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 :
  ∫⁻ (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₀
⊢ ∫⁻ (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:
rw [lintegral_indicator ((h𝓑𝓧 _ hB).inter hA), lintegral_indicator hA]

Premises used: MeasureTheory.lintegral_indicator, MeasurableSet.inter
-- 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
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∞)
⊢ ∫⁻ (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:
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
    Pi.one_apply, one_mul]

Premises used: MeasureTheory.lintegral_const, Pi.one_apply, MeasureTheory.Measure.restrict_apply, Set.univ_inter, one_mul, MeasurableSet.univ