awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
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 γ)
have h₁ : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a) ∧
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ.singularPart η : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a)
Tactic: rw [Measure.AbsolutelyContinuous.add_left_iff] at h
Cleared hypotheses: 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 : α
| @Measure.MutuallySingular.{u_2} γ 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 γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    @Measure.MutuallySingular.{u_2} γ mγ ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have conv_rhs : Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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 γ) ((η.withDensity (κ.rnDeriv η) : (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.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
Tactic: rw [h, zero_add]
-- 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 : α
h :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ⟂ₘ
    (η : (a : α) → Measure γ) a
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
have h₁ : @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a) ∧
  @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
Tactic: rw [Measure.MutuallySingular.add_left_iff] at h
Cleared hypotheses: 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 :
  @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
      ((η : (a : α) → Measure γ) a) ∧
    @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
have refine_2 : @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
  ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
Tactic: rw [← Measure.MutuallySingular.self_iff]
-- 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.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
Tactic: have h_eq_add := rnDeriv_add_singularPart κ η
-- 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 : α
h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Kernel.ext_iff, Measure.ext_iff] at h_eq_add
Cleared hypotheses: h_eq_add
-- 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 : α
h_eq_add :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : Eq (α := ℝ≥0∞)
  ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (κ.mutuallySingularSetSlice η a) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
Tactic: specialize h_eq_add a (mutuallySingularSetSlice κ η a)
    (measurableSet_mutuallySingularSetSlice κ η a)
Cleared hypotheses: h_eq_add
-- 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 : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : Eq (α := ℝ≥0∞)
  ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
Tactic: simp only [coe_add, Pi.add_apply, Measure.coe_add,
    withDensity_rnDeriv_mutuallySingularSetSlice κ η, zero_add] at h_eq_add
Cleared hypotheses: h_eq_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 : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
  Eq (α := ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [← h_eq_add]
-- 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.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
Tactic: have h_eq_add := rnDeriv_add_singularPart κ η
-- 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 : α
h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Kernel.ext_iff, Measure.ext_iff] at h_eq_add
Cleared hypotheses: h_eq_add
-- 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 : α
h_eq_add :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : Eq (α := ℝ≥0∞)
  ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (κ.mutuallySingularSetSlice η a)ᶜ :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
Tactic: specialize h_eq_add a (mutuallySingularSetSlice κ η a)ᶜ
    (measurableSet_mutuallySingularSetSlice κ η a).compl
Cleared hypotheses: h_eq_add
-- 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 : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have h_eq_add₁ : Eq (α := ℝ≥0∞)
  ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (κ.mutuallySingularSetSlice η a)ᶜ :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
Tactic: simp only [coe_add, Pi.add_apply, Measure.coe_add,
    singularPart_compl_mutuallySingularSetSlice κ η, add_zero] at h_eq_add
Cleared hypotheses: h_eq_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 : α
h_eq_add :
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
have rw : Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
  Eq (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (κ.mutuallySingularSetSlice η a)ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rw [← h_eq_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 η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α |
      Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a)}
have simp_rw : MeasurableSet.{u_1} (α := α)
  {a : α |
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)}
Tactic: simp_rw [← singularPart_eq_zero_iff_absolutelyContinuous,
    singularPart_eq_zero_iff_measure_eq_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 η
⊢ MeasurableSet.{u_1} (α := α)
    {a : α | @Measure.MutuallySingular.{u_2} γ mγ ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)}
have simp_rw : MeasurableSet.{u_1} (α := α)
  {a : α |
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)}
Tactic: simp_rw [← withDensity_rnDeriv_eq_zero_iff_mutuallySingular,
    withDensity_rnDeriv_eq_zero_iff_measure_eq_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 κ
⊢ κ.singularPart κ = 0
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ)
    (((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
Tactic: ext : 1
-- 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 κ
a : α
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ)
    (((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
have h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
Tactic: rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]
-- 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 κ
a : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart κ : (a : α) → Measure γ) a : Measure γ)
    (((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
have h₁ : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
Tactic: rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
have rw : (η.withDensity f + ξ : (a : α) → Measure γ) a =
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
Tactic: rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : @Measure.MutuallySingular.{u_2} γ mγ ((ξ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  (η.withDensity f + ξ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
⊢ (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
have rw₁ : HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑(η.withDensity f) : (a : α) → Measure γ)
    (⇑ξ : (a : α) → Measure γ) a =
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
Tactic: rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]