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 : α
suffices :
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal
      (1 - rnDerivAux κ (κ + η) a x)) a {x | 1 ≤ rnDerivAux κ (κ + η) a x} = 0 by
    rwa [withDensity_one_sub_rnDerivAux κ η] at this
-- 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 : α
simp_rw :
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp_rw [ofNNReal_toNNReal]

Premises used: ENNReal.ofNNReal_toNNReal
-- 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 : α
rw :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
rw₁ : MeasurableSet.{u_2} (α := γ) {x : γ | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}
rw₂ : Measurable (β := ℝ≥0∞) fun (b : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq, ae_restrict_iff]

Premises used: MeasureTheory.lintegral_eq_zero_iff, Filter.EventuallyEq, MeasureTheory.ae_restrict_iff, ProbabilityTheory.Kernel.withDensity_apply'
-- 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 : α
⊢ Measurable (β := ℝ≥0∞) fun (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)

Tactic:
fun_prop
-- 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 : α
⊢ MeasurableSet.{u_2} (α := γ) {x : γ | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}

Tactic:
exact (measurableSet_singleton 0).preimage (by fun_prop)

Premises used: MeasurableSet.preimage, MeasurableSingletonClass.measurableSet_singleton, OfNat.ofNat
-- 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 : α
⊢ Measurable (β := ℝ≥0∞) fun (b : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)

Tactic:
fun_prop
-- 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 : α
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))

Tactic:
fun_prop
-- 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 : α
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
ae_of_all _ (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- 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 : α
refine :
  ∀ (x : γ) (hx : Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x),
    ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x →
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
refine ae_of_all _ (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- 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 : α
x : γ
hx : 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
h :
  ∀ (x : α) (x_1 : γ),
    κ.rnDeriv η x x_1 = ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)
⊢ κ.rnDeriv η = fun (a : α) (x : γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
x : α
x_1 : γ
h h₁ :
  ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)
⊢ κ.rnDeriv η x x_1 = ENNReal.ofReal (κ.rnDerivAux (κ + η) x x_1) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x x_1)

Tactic:
rw [rnDeriv_def]

Premises used: ProbabilityTheory.Kernel.rnDeriv_def
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
simp_rw :
  Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦ κ.rnDeriv η p.1 p.2

Tactic:
simp_rw [rnDeriv_def]

Premises used: ProbabilityTheory.Kernel.rnDeriv_def
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)

Tactic:
(measurable_rnDerivAux κ _).ennreal_ofReal.div
    (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal

Premises used: ProbabilityTheory.Kernel.measurable_rnDerivAux, Measurable.ennreal_ofReal, Measurable.sub, Measurable.div, measurable_const
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)

Tactic:
exact (measurable_rnDerivAux κ _).ennreal_ofReal.div
    (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal

Premises used: ProbabilityTheory.Kernel.measurable_rnDerivAux, Measurable.ennreal_ofReal, Measurable.sub, Measurable.div, measurable_const
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable (β := ℝ≥0∞) fun (x : γ) ↦ κ.rnDeriv η a x

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
simp : 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x
⊢ κ.rnDeriv η a x = ∞ ↔ (a, x) ∈ κ.mutuallySingularSet η

Tactic:
simp only [rnDeriv, ENNReal.div_eq_top, ne_eq, ENNReal.ofReal_eq_zero, not_le,
    tsub_le_iff_right, zero_add, ENNReal.ofReal_ne_top, not_false_eq_true, and_true, or_false,
    mutuallySingularSet, mem_setOf_eq, and_iff_right_iff_imp]

Premises used: not_le, ENNReal.ofReal_eq_zero, and_true, ProbabilityTheory.Kernel.mutuallySingularSet, Set.mem_setOf_eq, ProbabilityTheory.Kernel.rnDeriv, zero_add, ne_eq, tsub_le_iff_right, ENNReal.div_eq_top, and_iff_right_iff_imp, or_false, ENNReal.ofReal_ne_top, not_false_eq_true
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x

Tactic:
fun h ↦ zero_lt_one.trans_le h

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x

Tactic:
exact fun h ↦ zero_lt_one.trans_le h

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
rw : (a, x) ∈ κ.mutuallySingularSet η ↔ x ∈ κ.mutuallySingularSetSlice η a
rw₁ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    x ∈ κ.mutuallySingularSetSlice η a
rw₂ :
  Membership.mem (γ := Set (α × γ)) {p : α × γ | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} (a, x) ↔
    Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
rw₃ : 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x
rw₄ rw₅ : 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ κ.rnDeriv η a x = ∞ ↔ x ∈ κ.mutuallySingularSetSlice η a

Tactic:
rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]

Premises used: ProbabilityTheory.Kernel.mutuallySingularSet, ProbabilityTheory.Kernel.rnDeriv_eq_top_iff, Set.mem_setOf, ProbabilityTheory.Kernel.mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    (↑(κ.rnDerivAux (κ + η) p.1 p.2).toNNReal : ℝ≥0∞) -
      (↑(1 - κ.rnDerivAux (κ + η) p.1 p.2).toNNReal : ℝ≥0∞) * κ.rnDeriv η p.1 p.2

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
change :
  Measurable.{u_2, 0} (α := γ) (β := ℝ≥0∞)
    (Function.comp (β := α × γ)
      (Function.uncurry fun (a : α) (b : γ) ↦
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b)
      fun (b : γ) ↦ (a, b))
⊢ Measurable (β := ℝ≥0∞) fun (x : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x

Tactic:
change Measurable ((Function.uncurry fun a b ↦
    ENNReal.ofReal (rnDerivAux κ (κ + η) a b)
    - ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a b) * rnDeriv κ η a b) ∘ (fun b ↦ (a, b)))

Premises used: HMul.hMul, ENNReal.ofReal, Measurable, HSub.hSub, Function.comp, Prod.mk, ProbabilityTheory.Kernel.rnDeriv, HAdd.hAdd, ProbabilityTheory.Kernel.rnDerivAux, Function.uncurry, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable.{u_2, 0} (α := γ) (β := ℝ≥0∞)
    (Function.comp (β := α × γ)
      (Function.uncurry fun (a : α) (b : γ) ↦
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b)
      fun (b : γ) ↦ (a, b))

Tactic:
(measurable_singularPart_fun κ η).comp measurable_prodMk_left

Premises used: Measurable.comp, ENNReal.ofReal, ProbabilityTheory.Kernel.measurable_singularPart_fun, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable.{u_2, 0} (α := γ) (β := ℝ≥0∞)
    (Function.comp (β := α × γ)
      (Function.uncurry fun (a : α) (b : γ) ↦
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b)
      fun (b : γ) ↦ (a, b))

Tactic:
exact (measurable_singularPart_fun κ η).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_singularPart_fun, measurable_prodMk_left
-- 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 :
  ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x
rw₁ :
  MeasurableSet.{u_2} (α := γ)
    {x : γ |
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
          (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x =
        0 x}
rw₂ :
  Measurable (β := ℝ≥0∞) fun (b : γ) ↦
    (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) - (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
        (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [singularPart, Kernel.withDensity_apply', lintegral_eq_zero_iff, EventuallyEq,
    ae_restrict_iff]

Premises used: MeasureTheory.lintegral_eq_zero_iff, Filter.EventuallyEq, ProbabilityTheory.Kernel.singularPart, MeasureTheory.ae_restrict_iff, ProbabilityTheory.Kernel.withDensity_apply'
-- 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 : α
⊢ MeasurableSet.{u_2} (α := γ)
    {x : γ |
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x}

Tactic:
measurableSet_preimage (measurable_singularPart_fun_right κ η a)
      (measurableSet_singleton _)

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ProbabilityTheory.Kernel.measurable_singularPart_fun_right, MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, WithTop.some, Set.preimage, Set.singleton, measurableSet_preimage
-- 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 : α
⊢ MeasurableSet.{u_2} (α := γ)
    {x : γ |
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x}

Tactic:
exact measurableSet_preimage (measurable_singularPart_fun_right κ η a)
      (measurableSet_singleton _)

Premises used: ProbabilityTheory.Kernel.measurable_singularPart_fun_right, MeasurableSingletonClass.measurableSet_singleton, measurableSet_preimage
-- 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 : α
⊢ Measurable (β := ℝ≥0∞) fun (b : γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b

Tactic:
measurable_singularPart_fun_right κ η a

Premises used: ENNReal.ofReal, ProbabilityTheory.Kernel.measurable_singularPart_fun_right
-- 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 : α
⊢ Measurable (β := ℝ≥0∞) fun (b : γ) ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b

Tactic:
exact measurable_singularPart_fun_right κ η a

Premises used: ProbabilityTheory.Kernel.measurable_singularPart_fun_right
-- 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 : α
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

Tactic:
measurable_singularPart_fun κ η

Premises used: ENNReal.ofReal, ProbabilityTheory.Kernel.measurable_singularPart_fun
-- 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 : α
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

Tactic:
exact measurable_singularPart_fun κ η

Premises used: ProbabilityTheory.Kernel.measurable_singularPart_fun
-- 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 : α
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
ae_of_all _ (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- 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 : α
refine :
  ∀ (x : γ) (hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ),
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
refine ae_of_all _ (fun x hx ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- 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 : α
x : γ
hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ κ.rnDerivAux (κ + η) a x < 1

Tactic:
simp only [mem_compl_iff, mutuallySingularSetSlice, mem_setOf, not_le] at hx

Premises used: not_le, Set.mem_setOf, ProbabilityTheory.Kernel.mutuallySingularSetSlice, Set.mem_compl_iff
-- 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 : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
simp_rw :
  ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    0 x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

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 γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
rw₁ : 0 ≤ 1 - κ.rnDerivAux (κ + η) a x
rw₂ : 0 < 1 - κ.rnDerivAux (κ + η) a x
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    0 x

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

Premises used: mul_inv_cancel₀, ENNReal.ofReal_div_of_pos, ENNReal.ofReal_mul, mul_assoc, tsub_self, Pi.zero_apply, div_eq_inv_mul, one_mul
-- 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 : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0

Tactic:
simp only [ne_eq, sub_eq_zero, hx.ne', not_false_eq_true]

Premises used: sub_eq_zero, ne_eq, LT.lt.ne', not_false_eq_true