awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
simp_rw :
  ((κ + η) ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((η ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
simp_rw₁ :
  (HAdd.hAdd (α := Kernel Unit β) (κ ∘ₖ Kernel.const Unit μ) (η ∘ₖ Kernel.const Unit μ) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((η ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
⊢ (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)

Tactic:
simp_rw [comp_eq_comp_const_apply, Kernel.comp_add_left, Kernel.add_apply]

Premises used: MeasureTheory.Measure.comp_eq_comp_const_apply, ProbabilityTheory.Kernel.add_apply, ProbabilityTheory.Kernel.comp_add_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
rw :
  (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
rw₁ rw₂ :
  HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ) =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
⊢ HAdd.hAdd (α := (a : α) → Measure β) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← Kernel.coe_add, add_comp]

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.add_comp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ (a • μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (β := Measure β) a ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (a • μ) = HSMul.hSMul (β := Measure β) a ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ (a • μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure β) a ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [bind_apply hs κ.aemeasurable, lintegral_smul_measure, smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.lintegral_smul_measure, ProbabilityTheory.Kernel.aemeasurable, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
⊢ AbsolutelyContinuous.{u_3} (α := γ) (_m0 := mγ) ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ((⇑κ : (a : α) → Measure γ) ∘ₘ ν)

Tactic:
Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
refine :
  ∀ (s : Set γ) (hs : MeasurableSet s)
    (hs_zero :
      Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AbsolutelyContinuous.{u_3} (α := γ) (_m0 := mγ) ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ((⇑κ : (a : α) → Measure γ) ∘ₘ ν)

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hs_zero :
      (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
        0),
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.lintegral_eq_zero_iff, ProbabilityTheory.Kernel.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0

Tactic:
hμν.ae_eq hs_zero

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero :
  (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0

Tactic:
exact hμν.ae_eq hs_zero

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)

Tactic:
Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
refine :
  ∀ (s : Set β) (hs : MeasurableSet s)
    (hs_zero :
      Eq (α := ℝ≥0∞) ((((⇑η : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((((⇑η : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀
    (hs_zero :
      (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
        0),
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.lintegral_eq_zero_iff, ProbabilityTheory.Kernel.aemeasurable, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
a : α
ha_zero : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞)
ha_ac : AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞)

Tactic:
ha_ac ha_zero
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (a : α) ↦ ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)) x)
                    (0 x))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (a : α) ↦
                        AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                          ((η : (a : α) → Measure β) a))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := ℝ≥0∞)
                          ((fun (a : α) ↦ ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞))
                            x)
                          (0 x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (a : α)
    (ha_zero : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞))
    (ha_ac :
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 a : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
hμν : μ ≪ ν
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ ν)

Tactic:
(AbsolutelyContinuous.comp_left μ hκη).trans (hμν.comp_right η)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.comp_left, MeasureTheory.Measure.AbsolutelyContinuous.comp_right, MeasureTheory.Measure.AbsolutelyContinuous.trans
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
rw :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) →
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) x)
        (sum fun (ω : α) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
            ((κ : (a : α) → Measure β) ω : Measure β))
⊢ ∀ᵐ (ω : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) ω) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [Measure.comp_eq_sum_of_countable, ae_iff_of_countable]

Premises used: MeasureTheory.Measure.comp_eq_sum_of_countable, MeasureTheory.ae_iff_of_countable
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
⊢ ∀ (x : α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) →
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) x)
        (sum fun (ω : α) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
            ((κ : (a : α) → Measure β) ω : Measure β))

Tactic:
fun ω hμω ↦ Measure.absolutelyContinuous_sum_right ω (Measure.absolutelyContinuous_smul hμω)

Premises used: MeasureTheory.Measure.absolutelyContinuous_smul, MeasureTheory.Measure.absolutelyContinuous_sum_right
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : Countable α
inst_1 : MeasurableSingletonClass α
⊢ ∀ (x : α),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞) →
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) x)
        (sum fun (ω : α) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure β) ((μ : (a : Set α) → ℝ≥0∞) {ω} : ℝ≥0∞)
            ((κ : (a : α) → Measure β) ω : Measure β))

Tactic:
exact fun ω hμω ↦ Measure.absolutelyContinuous_sum_right ω (Measure.absolutelyContinuous_smul hμω)

Premises used: MeasureTheory.Measure.absolutelyContinuous_smul, MeasureTheory.Measure.absolutelyContinuous_sum_right
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
h :
  ∀ (b : Bool),
    Eq (α := Measure β) ((κ ∘ₖ boolKernel μ ν : (a : Bool) → Measure β) b : Measure β)
      ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) b :
        Measure β)
⊢ κ ∘ₖ boolKernel μ ν = boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)

Tactic:
ext b : 1
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
b : Bool
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) false)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) false)
h₁ :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) true)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) true)
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) b)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) b)

Tactic:
cases b
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) false)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) false)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.bind.{u_1, u_2} (α := α) (mα := mα) ((boolKernel μ ν : (a : Bool) → Measure α) true)
      (⇑κ : (a : α) → Measure β))
    ((boolKernel ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν) : (a : Bool) → Measure β) true)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
              HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
            (a : Set α) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ (⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π =
    HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
      HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
h :
  ∫⁻ (a : Bool), (((Kernel.boolKernel μ ν : (a : Bool) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
    (HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
          HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
        (a : Set α) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞)
    ((((⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
            HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : Bool), (((Kernel.boolKernel μ ν : (a : Bool) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
    (HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) ν +
          HSMul.hSMul (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) μ :
        (a : Set α) → ℝ≥0∞)
      s

Tactic:
simp [lintegral_fintype, mul_comm]

Premises used: MeasureTheory.lintegral_fintype, mul_comm
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
π : Measure Bool
μ ν : Measure α
hπ : Ne (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {false} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ (⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π

Tactic:
boolKernel_comp_measure _ _ _ ▸ add_comm _ (π {true} • ν) ▸
    (Measure.absolutelyContinuous_smul hπ).add_right _

Premises used: ProbabilityTheory.boolKernel_comp_measure, Eq.rec, MeasureTheory.Measure.AbsolutelyContinuous.add_right, add_comm, MeasureTheory.Measure.absolutelyContinuous_smul, Bool.true, HSMul.hSMul, Singleton.singleton, Eq.symm, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
π : Measure Bool
μ ν : Measure α
hπ : Ne (α := ℝ≥0∞) ((π : (a : Set Bool) → ℝ≥0∞) {true} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ν ≪ (⇑(Kernel.boolKernel μ ν) : (a : Bool) → Measure α) ∘ₘ π

Tactic:
boolKernel_comp_measure _ _ _ ▸ (Measure.absolutelyContinuous_smul hπ).add_right _

Premises used: ProbabilityTheory.boolKernel_comp_measure, Eq.rec, MeasureTheory.Measure.AbsolutelyContinuous.add_right, MeasureTheory.Measure.absolutelyContinuous_smul, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
h₁ : ¬IsSFiniteKernel (mα := PUnit.instMeasurableSpace) (Kernel.const Unit μ)
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_left, Kernel.zero_apply]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left, ProbabilityTheory.Kernel.zero_apply, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h h₁ h₂ h₃ h₄ : ¬SFinite μ
⊢ ¬IsSFiniteKernel (mα := PUnit.instMeasurableSpace) (Kernel.const Unit μ)

Tactic:
rwa [Kernel.isSFiniteKernel_const]

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_const
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
h₁ : ¬IsSFiniteKernel (mα := Prod.instMeasurableSpace) (Kernel.prodMkLeft Unit κ)
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_right, Kernel.zero_apply]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right, ProbabilityTheory.Kernel.zero_apply, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h h₁ h₂ h₃ h₄ : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (mα := Prod.instMeasurableSpace) (Kernel.prodMkLeft Unit κ)

Tactic:
rwa [Kernel.isSFiniteKernel_prodMkLeft_unit]

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit