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 : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
inst_2 : IsFiniteKernel η
a : α
⊢ (κ + ν).rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)] κ.rnDeriv η a + ν.rnDeriv η a
have h : ∀ (x : γ)
  (h1 :
    (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
  (h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
  (h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
  (h4 :
    (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
            ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
        x =
      HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
        (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
        (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x),
  (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
Tactic: filter_upwards [(κ + ν).rnDeriv_eq_rnDeriv_measure, κ.rnDeriv_eq_rnDeriv_measure,
    ν.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_add (ν a) (η a)] with x h1 h2 h3 h4
-- 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h : Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
  (κ.rnDeriv η a + ν.rnDeriv η a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₁ : Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
  κ.rnDeriv η a x + ν.rnDeriv η a x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₂ : Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
h₂ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₃ : Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
h₂ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
h₃ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₄ : (∂HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑κ : (a : α) → Measure γ) (⇑ν : (a : α) → Measure γ)
        a/∂(η : (a : α) → Measure γ) a)
    x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
h₂ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
h₃ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₄ :
  (∂HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑κ : (a : α) → Measure γ)
          (⇑ν : (a : α) → Measure γ) a/∂(η : (a : α) → Measure γ) a)
      x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₅ : (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
        ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
    x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
h₂ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
h₃ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₄ :
  (∂HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑κ : (a : α) → Measure γ)
          (⇑ν : (a : α) → Measure γ) a/∂(η : (a : α) → Measure γ) a)
      x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₅ :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₆ : HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
    (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, 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 : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have rw : LE.le (α := ℝ≥0∞)
  (((Measure.withDensity ((η : (a : α) → Measure γ) a)
            (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply' _ s]
-- 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have rw : ∫⁻ (x : γ) in s,
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
      x ∂(η : (a : α) → Measure γ) a =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply _ hs, (κ a).withDensity_rnDeriv_eq _ 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
s : Set γ
hs : MeasurableSet s
rw :
  ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        x ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞)
  (((Measure.withDensity ((η : (a : α) → Measure γ) a)
            (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply _ hs, (κ a).withDensity_rnDeriv_eq _ 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
s : Set γ
hs : MeasurableSet s
rw :
  ∫⁻ (x : γ) in s,
      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
        x ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
rw₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.withDensity ((η : (a : α) → Measure γ) a)
              (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
have rw₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply _ hs, (κ a).withDensity_rnDeriv_eq _ 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ ∫⁻ (c : γ), κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have rw : ∫⁻ (x : γ) in univ, κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
Tactic: rw [← setLIntegral_univ, setLIntegral_rnDeriv h MeasurableSet.univ]
-- 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.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  ∫⁻ (x : γ) in univ, κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ ∫⁻ (c : γ), κ.rnDeriv η a c ∂(η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
  ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, setLIntegral_rnDeriv h MeasurableSet.univ]
-- 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 : α
⊢ LE.le.{u_2} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)
have refine : ∀ (s : Set γ) (hs : MeasurableSet s),
  s.Nonempty →
    LE.le (α := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine Measure.le_intro (fun 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
h : s.Nonempty
⊢ LE.le (α := ℝ≥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, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a ≤
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
Tactic: rw [Kernel.withDensity_apply']