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 : 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∞)
rw₃ 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∞)
⊢ 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 [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    singularPart_compl_mutuallySingularSetSlice, add_zero]

Premises used: MeasurableSet.compl, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, disjoint_compl_right, MeasureTheory.measure_union, ProbabilityTheory.Kernel.singularPart_compl_mutuallySingularSetSlice, add_zero
-- 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 :
  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∞)
⊢ 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 [← Measure.measure_univ_eq_zero]

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

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

Tactic:
have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp
-- 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 : α
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∞)
rw₃ 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∞)
⊢ 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 [this, measure_union disjoint_compl_right (measurableSet_mutuallySingularSetSlice κ η a).compl,
    withDensity_rnDeriv_mutuallySingularSetSlice, zero_add]

Premises used: zero_add, MeasurableSet.compl, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlice, disjoint_compl_right, MeasureTheory.measure_union, ProbabilityTheory.Kernel.withDensity_rnDeriv_mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
rw :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a
| Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.coe_add, Pi.add_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 : α
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
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.coe_add, Pi.add_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 : α
⊢ 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:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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_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
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 γ)
⊢ 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 ↦ ?_⟩
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
refine_1 :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a)
⊢ HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a

Tactic:
rw [h, add_zero]

Premises used: add_zero
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a)

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: ProbabilityTheory.Kernel.withDensity_absolutelyContinuous
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η : (a : α) → Measure γ) a)

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: ProbabilityTheory.Kernel.withDensity_absolutelyContinuous
-- 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 : α
h :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ≪
    (η : (a : α) → Measure γ) a
⊢ 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

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff
-- 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 : α
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)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)

Tactic:
Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2
    (mutuallySingular_singularPart _ _ _)

Premises used: ProbabilityTheory.Kernel.mutuallySingular_singularPart, MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular, And.right
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
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)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)

Tactic:
exact Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2
    (mutuallySingular_singularPart _ _ _)

Premises used: ProbabilityTheory.Kernel.mutuallySingular_singularPart, MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular, And.right
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
rw :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ⟂ₘ
    (η : (a : α) → Measure γ) a
| @Measure.MutuallySingular.{u_2} γ mγ ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.coe_add, Pi.add_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 : α
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
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ) ↔
    @Measure.MutuallySingular.{u_2} γ mγ ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]

Premises used: ProbabilityTheory.Kernel.rnDeriv_add_singularPart, ProbabilityTheory.Kernel.coe_add, Pi.add_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 : α
⊢ 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:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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_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
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 γ)
⊢ 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 ↦ ?_⟩
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
refine_1 :
  @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ⟂ₘ
    (η : (a : α) → Measure γ) a

Tactic:
rw [h, zero_add]

Premises used: zero_add
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
mutuallySingular_singularPart _ _ _

Premises used: ProbabilityTheory.Kernel.mutuallySingular_singularPart
-- 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 : α
h : Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)
⊢ @Measure.MutuallySingular.{u_2} γ mγ ((κ.singularPart η : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)

Tactic:
exact mutuallySingular_singularPart _ _ _

Premises used: ProbabilityTheory.Kernel.mutuallySingular_singularPart
-- 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 : α
h :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
      ((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) ⟂ₘ
    (η : (a : α) → Measure γ) a
⊢ @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

Premises used: MeasureTheory.Measure.MutuallySingular.add_left_iff
-- 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 : α
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)
refine_2 :
  @Measure.MutuallySingular.{u_2} γ mγ ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
    ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) (0 : Measure γ)

Tactic:
rw [← Measure.MutuallySingular.self_iff]

Premises used: MeasureTheory.Measure.MutuallySingular.self_iff