awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1

Tactic:
Measure.ae_ae_of_ae_compProd (p := fun x ↦ κ.rnDeriv η x.1 x.2 = 1) ?_

Premises used: MeasureTheory.Measure.ae_ae_of_ae_compProd
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
refine : ∀ᵐ (x : α × β) ∂μ ⊗ₘ η, (fun (x : α × β) ↦ κ.rnDeriv η x.1 x.2 = 1) x
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((η : (a : α) → Measure β) a : Measure β), κ.rnDeriv η a b = 1

Tactic:
refine Measure.ae_ae_of_ae_compProd (p := fun x ↦ κ.rnDeriv η x.1 x.2 = 1) ?_

Premises used: MeasureTheory.Measure.ae_ae_of_ae_compProd
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ Measurable (β := ℝ≥0∞) fun (x : α × β) ↦ κ.rnDeriv η x.1 x.2

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
⊢ Measurable (β := ℝ≥0∞) fun (x : α × β) ↦ 1

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
refine :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ∫⁻ (x : α × β) in s, 1 ∂μ ⊗ₘ η
⊢ ∀ᵐ (x : α × β) ∂μ ⊗ₘ η, (fun (x : α × β) ↦ κ.rnDeriv η x.1 x.2 = 1) x

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (by fun_prop) fun s hs _ ↦ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp : ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = ∫⁻ (x : α × β) in s, 1 ∂μ ⊗ₘ η

Tactic:
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply,
    Set.univ_inter, one_mul]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, one_mul, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Measurable (Function.uncurry (κ.rnDeriv η))
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]

Premises used: MeasureTheory.Measure.compProd_withDensity, MeasureTheory.Measure.compProd_congr, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ : Eq (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [h]
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac :
  ∀ᵐ (a : α) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
hκ_eq :
  ∀ᵐ (a : α) ∂μ,
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β)
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
calc : ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s
calc₁ : Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η = (μ ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
calc ∫⁻ x in s, κ.rnDeriv η x.1 x.2 ∂μ ⊗ₘ η
  _ = (μ ⊗ₘ κ) s := by
    rw [Measure.compProd_congr hκ_eq, Measure.compProd_withDensity, withDensity_apply _ hs]
    fun_prop
  _ = (μ ⊗ₘ η) s := by rw [h]

Premises used: MeasureTheory.Measure.compProd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.CompProdEqIff
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : MeasurableSpace.CountableOrCountablyGenerated α β
inst_1 : IsFiniteMeasure μ
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
⊢ μ ⊗ₘ κ = μ ⊗ₘ η ↔
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)

Tactic:
⟨Kernel.ae_eq_of_compProd_eq, Measure.compProd_congr⟩

Premises used: ProbabilityTheory.Kernel.ae_eq_of_compProd_eq, MeasureTheory.Measure.compProd_congr, Iff.intro
-- 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)
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
by_cases hμ : SFinite μ

Premises used: MeasureTheory.SFinite
-- 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 μ
neg : 0 ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hμ]

Premises used: MeasureTheory.Measure.compProd_of_not_sfinite
-- 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 μ
⊢ 0 ⟂ₘ ν ⊗ₘ η

Tactic:
simp
-- 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 μ
pos : ∀ (hν : SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
neg : ∀ (hν : ¬SFinite ν), μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
by_cases hν : SFinite ν

Premises used: MeasureTheory.SFinite
-- 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 ν
neg : μ ⊗ₘ κ ⟂ₘ 0
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
rw [compProd_of_not_sfinite _ _ hν]

Premises used: MeasureTheory.Measure.compProd_of_not_sfinite
-- 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 ν
⊢ μ ⊗ₘ κ ⟂ₘ 0

Tactic:
simp
-- 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 η
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η
-- 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
pos : ν ⊗ₘ η ⟂ₘ μ ⊗ₘ κ
⊢ μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η

Tactic:
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)
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
⊢ ν ⊗ₘ η ⟂ₘ μ ⊗ₘ κ

Tactic:
⟨s, hs, ?_⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- 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
pos :
  Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ν ⊗ₘ η ⟂ₘ μ ⊗ₘ κ

Tactic:
refine ⟨s, hs, ?_⟩
-- 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
pos :
  ∫⁻ (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
⊢ Eq (α := ℝ≥0∞) ((ν ⊗ₘ η : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [compProd_apply hs, compProd_apply hs.compl]

Premises used: MeasureTheory.Measure.compProd_apply, MeasurableSet.compl
-- 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
⊢ ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a

Tactic:
have h_eq a : Prod.mk a ⁻¹' s = Kernel.mutuallySingularSetSlice κ η a := rfl
-- 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
a : α
rw :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [h_eq, Kernel.measure_mutuallySingularSetSlice]

Premises used: ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice
-- 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
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
-- 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∞)
h :
  ∀ (a : α) (ha : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
filter_upwards [hκη] with a ha
-- 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∞)
a : α
ha : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
h₁ : Eq.{u_2 + 1} (α := Measure β) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure β) a : Measure β) (0 : Measure β)
h₂ h₃ h₄ h₅ : @MutuallySingular.{u_2} β mβ ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
      Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]

Premises used: ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular
-- 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∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
have h2 : ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s)ᶜ = 0 := by
    filter_upwards [hκη] with a ha
    rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
      Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]