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 γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ 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∞)
have 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∞)
Tactic: rw [← Measure.measure_univ_eq_zero]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
⊢ 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∞)
have this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
Tactic: have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    singularPart_compl_mutuallySingularSetSlice, add_zero]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ 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∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞) =
    0 ↔
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    singularPart_compl_mutuallySingularSetSlice, add_zero]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a)ᶜ :
          ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ 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∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) =
    0 ↔
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    singularPart_compl_mutuallySingularSetSlice, add_zero]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a)ᶜ :
          ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        (0 : ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ 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∞)
have rw₃ : Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    singularPart_compl_mutuallySingularSetSlice, add_zero]
-- 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 : α
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞) ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
    (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [← Measure.measure_univ_eq_zero]
-- 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 : α
⊢ Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
Tactic: have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp
-- 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 : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]
-- 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 : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞) =
    0 ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]
-- 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 : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a)ᶜ :
          ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞) =
    0 ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]
-- 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 : α
this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ
rw :
  Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a)ᶜ :
          ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (κ.mutuallySingularSetSlice η a)ᶜ :
          ℝ≥0∞) =
      0 ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (κ.mutuallySingularSetSlice η a)ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]
-- 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have rw : HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
  (η : (a : α) → Measure γ) a
Tactic: rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]
-- 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 : α
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have conv_rhs : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a
Tactic: conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]
-- 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 : α
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
        ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
      (η : (a : α) → Measure γ) a
have refine_1 : ∀ (h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)),
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : α
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)),
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
        ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
      (η : (a : α) → Measure γ) a
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
        ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
      (η : (a : α) → Measure γ) a
have refine_2 : ∀
  (h :
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
        ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
      (η : (a : α) → Measure γ) a),
  Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a
have refine_1 : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
  ((η : (a : α) → Measure γ) a)
Tactic: rw [h, add_zero]