awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h2 :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α), (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0

Tactic:
simp [h1, lintegral_congr_ae h2]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
(MutuallySingular.compProd_of_right _ _ ?_).symm

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_right, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
refine : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((η : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a)
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
refine (MutuallySingular.compProd_of_right _ _ ?_).symm

Premises used: MeasureTheory.Measure.MutuallySingular.compProd_of_right, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη simp_rw : ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ ∀ᵐ (a : α) ∂ν, @MutuallySingular.{u_2} β mβ ((η : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a)

Tactic:
simp_rw [MutuallySingular.comm, hκη]

Premises used: MeasureTheory.Measure.MutuallySingular.comm
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
⊢ μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η ↔
    ∀ᵐ (a : α) ∂μ, @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
⟨fun h ↦ mutuallySingular_of_mutuallySingular_compProd h AbsolutelyContinuous.rfl
    AbsolutelyContinuous.rfl, MutuallySingular.compProd_of_right _ _⟩

Premises used: MeasureTheory.Measure.mutuallySingular_of_mutuallySingular_compProd, MeasureTheory.Measure.MutuallySingular.compProd_of_right, Iff.intro, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this :
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
h₁ :
  ∀ (a : α)
    (ha : Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)),
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
filter_upwards [this] with a ha
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
this :
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
a : α
ha : Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
h₁ h₂ h₃ h₄ :
  ∀ (ha : AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha

Premises used: ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
suffices :
  ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by
    filter_upwards [this] with a ha
    rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η

Tactic:
rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff, MeasureTheory.Measure.compProd_add_right
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
⊢ μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η

Tactic:
have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
    MutuallySingular.compProd_of_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
compProd_eq_zero_iff.mp ?_

Premises used: Iff.mp, MeasureTheory.Measure.compProd_eq_zero_iff
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
refine : μ ⊗ₘ κ.singularPart η = 0
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
refine compProd_eq_zero_iff.mp ?_

Premises used: Iff.mp, MeasureTheory.Measure.compProd_eq_zero_iff
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ.singularPart η = 0

Tactic:
eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this

Premises used: MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular, And.right
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ.singularPart η = 0

Tactic:
exact eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this

Premises used: MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular, And.right
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
inst_4 : SFinite ν
inst_5 : ∀ (a : α), NeZero.{u_2} (R := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔
    μ ≪ ν ∧
      ∀ᵐ (a : α) ∂μ,
        AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
⟨fun h ↦ ⟨absolutelyContinuous_of_compProd h, h.kernel_of_compProd⟩, fun h ↦ h.1.compProd h.2⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd, MeasureTheory.Measure.absolutelyContinuous_of_compProd, MeasureTheory.Measure.AbsolutelyContinuous.compProd, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔
    ∀ᵐ (a : α) ∂μ,
      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)

Tactic:
⟨AbsolutelyContinuous.kernel_of_compProd, AbsolutelyContinuous.compProd_right⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd, MeasureTheory.Measure.AbsolutelyContinuous.compProd_right, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
h :
  ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ deterministic f hf ∘ₖ κ = κ.map f

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₁ :
  ∫⁻ (b : β),
      (((deterministic f hf : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
h₂ :
  ∫⁻ (b : β), s.indicator (fun (x : γ) ↦ 1) (f b) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
h₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasureTheory.lintegral_indicator_const_comp, ProbabilityTheory.Kernel.deterministic_apply', ProbabilityTheory.Kernel.comp_apply', one_mul
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
h :
  ∀ (a : γ) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ ∘ₖ deterministic g hg = κ.comap g hg

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∫⁻ (b : α),
      (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s ∂(deterministic g hg : (a : γ) → Measure α) a =
    (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s
h₂ :
  ∫⁻ (b : α), (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s ∂Measure.dirac (g a) =
    (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]

Premises used: MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply', ProbabilityTheory.Kernel.comap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
h :
  ∀ (a : β) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((deterministic g hg ∘ₖ deterministic f hf : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s :
          ℝ≥0∞)
        ((((deterministic (g ∘ f) ⋯ : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ deterministic g hg ∘ₖ deterministic f hf = deterministic (g ∘ f) ⋯

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
a : β
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic g hg ∘ₖ deterministic f hf : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic (g ∘ f) ⋯ : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [comp_deterministic_eq_comap, comap_apply, deterministic_apply]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.comap_apply, ProbabilityTheory.Kernel.comp_deterministic_eq_comap
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
simp_rw : Eq (α := Kernel (β × α) (β × α)) (deterministic Prod.swap ⋯ ∘ₖ deterministic Prod.swap ⋯) Kernel.id
simp_rw₁ : Eq (α := Kernel (β × α) (β × α)) (deterministic (Prod.swap ∘ Prod.swap) ⋯) Kernel.id
simp_rw₂ : Eq (α := Kernel (β × α) (β × α)) (deterministic id ⋯) Kernel.id
⊢ Eq (α := Kernel (β × α) (β × α)) (swap α β ∘ₖ swap β α) Kernel.id

Tactic:
simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.id, Prod.swap_swap_eq, ProbabilityTheory.Kernel.swap
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
rw : deterministic Prod.swap ⋯ ∘ₖ κ = κ.map Prod.swap
rw₁ rw₂ : Eq (α := Kernel α (γ × β)) (κ.map Prod.swap) (κ.map Prod.swap)
⊢ swap β γ ∘ₖ κ = κ.map Prod.swap

Tactic:
rw [swap, deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.swap
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
pos : ∀ (hf : Measurable f), Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
pos :
  ∀ (a : α) (s : Set δ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((((η ∘ₖ κ).map f : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((η.map f ∘ₖ κ : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
pos :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (f ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ((((η.map f : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) a
pos₁ : MeasurableSet (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((((η ∘ₖ κ).map f : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((η.map f ∘ₖ κ : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply' _ hf _ hs, comp_apply', comp_apply' _ _ _ hs]

Premises used: ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (f ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ((((η.map f : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [map_apply' _ hf _ hs]

Premises used: ProbabilityTheory.Kernel.map_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
hf hs
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
exact hf hs
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : ¬Measurable f
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)

Tactic:
simp [map_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
h :
  ∀ (x : α) (s : Set δ) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((η ∘ₖ κ.map f : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η.comap f hf ∘ₖ κ : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ η ∘ₖ κ.map f = η.comap f hf ∘ₖ κ

Tactic:
ext x s ms
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
h :
  ∫⁻ (a : β), (((η : (a : γ) → Measure δ) (f a) : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      (((η.comap f hf : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ.map f : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η.comap f hf ∘ₖ κ : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comp_apply' _ _ _ ms, lintegral_map _ hf _ (η.measurable_coe ms), comp_apply' _ _ _ ms]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply'