awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
exact measurable_rnDeriv _ _

Premises used: ProbabilityTheory.Kernel.measurable_rnDeriv
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
simp_rw :
  ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) /
          ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
simp_rw [rnDeriv]

Premises used: ProbabilityTheory.Kernel.rnDeriv
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
simp_rw : ∀ x ∈ s, x ∉ κ.mutuallySingularSetSlice η a
⊢ ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1

Tactic:
simp_rw [← notMem_mutuallySingularSetSlice]

Premises used: ProbabilityTheory.Kernel.notMem_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ ∀ x ∈ s, x ∉ κ.mutuallySingularSetSlice η a

Tactic:
fun x hx hx_mem ↦ hs hx hx_mem

Premises used: Not
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ ∀ x ∈ s, x ∉ κ.mutuallySingularSetSlice η a

Tactic:
exact fun x hx hx_mem ↦ hs hx hx_mem
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
⊢ ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1

Tactic:
have hs' : ∀ x ∈ s, rnDerivAux κ (κ + η) a x < 1 := by
    simp_rw [← notMem_mutuallySingularSetSlice]
    exact fun x hx hx_mem ↦ hs hx hx_mem
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
⊢ ∫⁻ (x : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) /
          ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η : (a : α) → Measure γ) a

Tactic:
setLIntegral_congr_fun hsm (fun x hx ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
refine :
  ∀ (x : γ) (hx : x ∈ s),
    (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)
⊢ ∫⁻ (x : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) /
          ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η : (a : α) → Measure γ) a

Tactic:
refine setLIntegral_congr_fun hsm (fun x hx ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
rw₁ : 0 ≤ 1 - κ.rnDerivAux (κ + η) a x
rw₂ : 0 < 1 - κ.rnDerivAux (κ + η) a x
⊢ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)

Tactic:
rw [ofNNReal_toNNReal, ← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul,
        ← mul_assoc, mul_inv_cancel₀, one_mul]

Premises used: ENNReal.ofNNReal_toNNReal, mul_inv_cancel₀, ENNReal.ofReal_div_of_pos, ENNReal.ofReal_mul, mul_assoc, div_eq_inv_mul, one_mul
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
rw : ¬1 = κ.rnDerivAux (κ + η) a x
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0

Tactic:
rw [ne_eq, sub_eq_zero]

Premises used: sub_eq_zero, ne_eq
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ ¬1 = κ.rnDerivAux (κ + η) a x

Tactic:
(hs' x hx).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ ¬1 = κ.rnDerivAux (κ + η) a x

Tactic:
exact (hs' x hx).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

Tactic:
simp [(hs' x hx).le]

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
simp [hs' x hx]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
setLIntegral_rnDerivAux κ η a hsm

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDerivAux
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x :
  ∫⁻ (x : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) /
          ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) ∂(κ + η : (a : α) → Measure γ) a =
    ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η : (a : α) → Measure γ) a
⊢ ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) /
          ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
calc
    ∫⁻ x in s, ↑(Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) *
      (ENNReal.ofReal (rnDerivAux κ (κ + η) a x) /
        ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x)) ∂(κ + η) a
  _ = ∫⁻ x in s, ENNReal.ofReal (rnDerivAux κ (κ + η) a x) ∂(κ + η) a := by
      refine setLIntegral_congr_fun hsm (fun x hx ↦ ?_)
      rw [ofNNReal_toNNReal, ← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul,
        ← mul_assoc, mul_inv_cancel₀, one_mul]
      · rw [ne_eq, sub_eq_zero]
        exact (hs' x hx).ne'
      · simp [(hs' x hx).le]
      · simp [hs' x hx]
  _ = κ a s := setLIntegral_rnDerivAux κ η a hsm

Premises used: HAdd.hAdd, DFunLike.coe, ProbabilityTheory.Kernel.setLIntegral_rnDerivAux
-- 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 : α
symm : @Measure.MutuallySingular.{u_2} γ mγ ((η : (a : α) → Measure γ) a) ((κ.singularPart η : (a : α) → Measure γ) a)
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
symm
-- 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 : α
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((η : (a : α) → Measure γ) a) ((κ.singularPart η : (a : α) → Measure γ) a)

Tactic:
⟨mutuallySingularSetSlice κ η a, measurableSet_mutuallySingularSetSlice κ η a,
    measure_mutuallySingularSetSlice κ η a, singularPart_compl_mutuallySingularSetSlice κ η a⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, Exists.intro, ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice, ProbabilityTheory.Kernel.measure_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 : α
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((η : (a : α) → Measure γ) a) ((κ.singularPart η : (a : α) → Measure γ) a)

Tactic:
exact ⟨mutuallySingularSetSlice κ η a, measurableSet_mutuallySingularSetSlice κ η a,
    measure_mutuallySingularSetSlice κ η a, singularPart_compl_mutuallySingularSetSlice κ η a⟩
-- 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 η
h :
  ∀ (a : α) (s : Set γ) (hs : 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∞)
⊢ η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ

Tactic:
ext a s hs
-- 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 : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← inter_union_diff s (mutuallySingularSetSlice κ η a)]

Premises used: Set.inter_union_diff, 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 : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (κ.mutuallySingularSetSlice η a)

Tactic:
have hm := measurableSet_mutuallySingularSetSlice κ η a
-- 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 : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)

Tactic:
simp only [measure_union (Disjoint.mono inter_subset_right le_rfl disjoint_sdiff_right)
    (hs.diff hm)]

Premises used: MeasurableSet.diff, le_rfl, Set.disjoint_sdiff_right, MeasureTheory.measure_union, Disjoint.mono, Set.inter_subset_right
-- 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 : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ s ⊆ κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
rw :
  Eq (α := ℝ≥0∞) ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    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∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
rw [← Measure.measure_univ_eq_zero]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp