awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h :
  @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
      ((η : (a : α) → Measure γ) a) ∧
    @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)

Tactic:
h.1.mono_ac Measure.AbsolutelyContinuous.rfl
    (withDensity_absolutelyContinuous (κ := η) (rnDeriv κ η) a)

Premises used: ProbabilityTheory.Kernel.withDensity_absolutelyContinuous, ProbabilityTheory.Kernel.rnDeriv, And.left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h :
  @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
      ((η : (a : α) → Measure γ) a) ∧
    @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)

Tactic:
exact h.1.mono_ac Measure.AbsolutelyContinuous.rfl
    (withDensity_absolutelyContinuous (κ := η) (rnDeriv κ η) a)

Premises used: ProbabilityTheory.Kernel.withDensity_absolutelyContinuous, ProbabilityTheory.Kernel.rnDeriv, And.left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
⊢ η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ

Tactic:
have h_eq_add := rnDeriv_add_singularPart κ η
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
⊢ ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [Kernel.ext_iff, Measure.ext_iff] at h_eq_add

Premises used: MeasureTheory.Measure.ext_iff, ProbabilityTheory.Kernel.ext_iff
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)

Tactic:
specialize h_eq_add a (mutuallySingularSetSlice κ η a)
    (measurableSet_mutuallySingularSetSlice κ η a)

Premises used: ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, ProbabilityTheory.Kernel.mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, Measure.coe_add,
    withDensity_rnDeriv_mutuallySingularSetSlice κ η, zero_add] at h_eq_add

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.coe_add, zero_add, Pi.add_apply, ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
rw :
  Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
rw [← h_eq_add]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
singularPart_eq_zero_iff_apply_eq_zero κ η a

Premises used: ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
exact singularPart_eq_zero_iff_apply_eq_zero κ η a

Premises used: ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)

Tactic:
specialize h_eq_add a (mutuallySingularSetSlice κ η a)ᶜ
    (measurableSet_mutuallySingularSetSlice κ η a).compl

Premises used: Compl.compl, MeasurableSet.compl, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, ProbabilityTheory.Kernel.mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, Measure.coe_add,
    singularPart_compl_mutuallySingularSetSlice κ η, add_zero] at h_eq_add

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.coe_add, Pi.add_apply, ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice, add_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
rw :
  Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
rw [← h_eq_add]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
withDensity_rnDeriv_eq_zero_iff_apply_eq_zero κ η a

Premises used: ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
exact withDensity_rnDeriv_eq_zero_iff_apply_eq_zero κ η a

Premises used: ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
simp_rw :
  MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a)}

Tactic:
simp_rw [← singularPart_eq_zero_iff_absolutelyContinuous,
    singularPart_eq_zero_iff_measure_eq_zero]

Premises used: ProbabilityTheory.Kernel.singularPart_eq_zero_iff_measure_eq_zero, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
        (0 : ℝ≥0∞)}

Tactic:
measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η)
    (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, ProbabilityTheory.Kernel.mutuallySingularSet, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, Set.preimage, Set.singleton, OfNat.ofNat, ProbabilityTheory.Kernel.mutuallySingularSetSlice, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
        (0 : ℝ≥0∞)}

Tactic:
exact measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η)
    (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, OfNat.ofNat, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
simp_rw :
  MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)}
⊢ MeasurableSet.{u_1} (α := α)
    {a : α | @Measure.MutuallySingular.{u_2} γ mγ ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)}

Tactic:
simp_rw [← withDensity_rnDeriv_eq_zero_iff_mutuallySingular,
    withDensity_rnDeriv_eq_zero_iff_measure_eq_zero]

Premises used: ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)}

Tactic:
measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η).compl
    (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, MeasurableSet.compl, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, Set.preimage, Set.singleton, OfNat.ofNat, ProbabilityTheory.Kernel.mutuallySingularSetSlice, Not, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)}

Tactic:
exact measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η).compl
    (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.compl, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, OfNat.ofNat, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst : IsFiniteKernel κ
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ)
      (((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
⊢ κ.singularPart κ = 0

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ : Kernel α γ
inst : IsFiniteKernel κ
a : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
h₁ h₂ :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ)
    (((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)

Tactic:
rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]

Premises used: ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous, ProbabilityTheory.Kernel.zero_apply
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  (η.withDensity f + ξ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
rw₁ :
  HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑(η.withDensity f) : (a : α) → Measure γ)
      (⇑ξ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
rw₂ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity f : (a : α) → Measure γ) a : Measure γ)
      ((ξ : (a : α) → Measure γ) a : Measure γ) =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
rw₃ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
      ((ξ : (a : α) → Measure γ) a : Measure γ) =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
rw₄ rw₅ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a)) =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))

Tactic:
rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]

Premises used: ProbabilityTheory.Kernel.coe_add, add_comm, Pi.add_apply, ProbabilityTheory.Kernel.withDensity_apply
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))

Tactic:
have : κ a = ξ a + (η a).withDensity (f a) := by
    rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
this :
  (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ f a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
(κ a).eq_rnDeriv₀ (hf.comp measurable_prodMk_left).aemeasurable hξ this

Premises used: Measurable.aemeasurable, Measurable.comp, MeasureTheory.Measure.eq_rnDeriv₀, measurable_prodMk_left