awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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)ᶜ
⊢ (η.withDensity fun (a : α) (x : γ) ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
      fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
have e_κ : η = (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
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)ᶜ
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have this : η.withDensity (κ.rnDeriv η) =
  ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)).withDensity
    (κ.rnDeriv η)
Tactic: have : withDensity η (rnDeriv κ η)
      = withDensity (withDensity (κ + η)
        (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))) (rnDeriv κ η) := by
    rw [rnDeriv_def']
    congr
    exact (withDensity_one_sub_rnDerivAux κ η).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 η)
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (b : γ) in s, (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [this, ← withDensity_mul, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 η)
rw :
  ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hf : Measurable (α := α × γ) (β := ℝ≥0∞)
  (Function.uncurry fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
Tactic: rw [this, ← withDensity_mul, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 η)
rw :
  ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hf₁ : Measurable (α := α × γ) (β := ℝ≥0) (Function.uncurry fun (a : α) (x : γ) ↦ (1 - κ.rnDerivAux (κ + η) a x).toNNReal)
Tactic: rw [this, ← withDensity_mul, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 η)
rw :
  ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
hf :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x)
hf₁ :
  Measurable (α := α × γ) (β := ℝ≥0) (Function.uncurry fun (a : α) (x : γ) ↦ (1 - κ.rnDerivAux (κ + η) a x).toNNReal)
⊢ Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hg : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [this, ← withDensity_mul, Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 η)
⊢ ∫⁻ (b : γ) in s,
      (↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) * κ.rnDeriv η a b ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have 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
Tactic: simp_rw [rnDeriv]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
have simp_rw : ∀ x ∈ s, x ∉ κ.mutuallySingularSetSlice η a
Tactic: simp_rw [← notMem_mutuallySingularSetSlice]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
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 η)
⊢ ∫⁻ (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
have hs' : ∀ 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
have 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)
Tactic: refine setLIntegral_congr_fun hsm (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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).toNNReal : ℝ≥0∞) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)
have rw : 1 - κ.rnDerivAux (κ + η) a x ≠ 0
Tactic: rw [ofNNReal_toNNReal, ← ENNReal.ofReal_div_of_pos, div_eq_inv_mul, ← ENNReal.ofReal_mul,
        ← mul_assoc, mul_inv_cancel₀, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
⊢ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)
have rw₁ : 0 ≤ 1 - κ.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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
⊢ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) *
      (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) =
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)
have rw₂ : 0 < 1 - κ.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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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 ≠ 0
have rw : ¬1 = κ.rnDerivAux (κ + η) a x
Tactic: rw [ne_eq, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
⊢ ∫⁻ (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
have 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: 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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γ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have symm : @Measure.MutuallySingular.{u_2} γ mγ ((η : (a : α) → Measure γ) a) ((κ.singularPart η : (a : α) → Measure γ) a)
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [← inter_union_diff s (mutuallySingularSetSlice κ η a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
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
⊢ 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)
have hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
Tactic: have hm := measurableSet_mutuallySingularSetSlice κ η a
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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)
⊢ 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)
have 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∞)
Tactic: simp only [measure_union (Disjoint.mono inter_subset_right le_rfl disjoint_sdiff_right)
    (hs.diff hm)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
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)
⊢ 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∞)
have 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∞)
      ((((κ : (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∞)
Tactic: rw [singularPart_of_subset_mutuallySingularSetSlice (hs.inter hm) inter_subset_right,
    singularPart_of_subset_compl_mutuallySingularSetSlice (diff_subset_iff.mpr (by simp)),
    add_zero, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice inter_subset_right,
    zero_add, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice (hs.diff hm)
      (diff_subset_iff.mpr (by simp)), add_comm]