awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
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))
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))
⊢ (κ : (a : α) → Measure γ) a =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
have rw₂ : HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity f : (a : α) → Measure γ) a : Measure γ)
    ((ξ : (a : α) → Measure γ) a : Measure γ) =
  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))
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))
rw₂ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity f : (a : α) → Measure γ) a : Measure γ)
      ((ξ : (a : α) → Measure γ) a : Measure γ) =
    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 (α := Measure γ) (β := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
    ((ξ : (a : α) → Measure γ) a : Measure γ) =
  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))
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))
rw₂ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((η.withDensity f : (a : α) → Measure γ) a : Measure γ)
      ((ξ : (a : α) → Measure γ) a : Measure γ) =
    HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
      (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
rw₃ :
  HAdd.hAdd (α := Measure γ) (β := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
      ((ξ : (a : α) → Measure γ) a : Measure γ) =
    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 (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a) (f 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 (hypothesis)
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)
⊢ f a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have this : (κ : (a : α) → Measure γ) a =
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
Tactic: have : κ a = ξ a + (η a).withDensity (f a) := by
    rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) : Measure γ)
have this : (κ : (a : α) → Measure γ) a =
  HAdd.hAdd (α := Measure γ) (β := Measure γ) ((ξ : (a : α) → Measure γ) a : Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a) (f a))
Tactic: have : κ a = ξ a + (η a).withDensity (f a) := by
    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 α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
⊢ IsFiniteKernel (η.withDensity (κ.rnDeriv η))
have refine : ∀ (a : α), (((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
Tactic: refine ⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ (((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
have rw : ∫⁻ (x : γ), κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a ≤ κ.bound
Tactic: rw [Kernel.withDensity_apply', setLIntegral_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
rw : ∫⁻ (x : γ), κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a ≤ κ.bound
⊢ (((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
have hf : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [Kernel.withDensity_apply', setLIntegral_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ ∫⁻ (x : γ), κ.rnDeriv η a x ∂(η : (a : α) → Measure γ) a ≤ κ.bound
have rw : ∫⁻ (a_1 : γ),
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
      a_1 ∂(η : (a : α) → Measure γ) a ≤
  κ.bound
Tactic: rw [lintegral_congr_ae rnDeriv_eq_rnDeriv_measure]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
⊢ IsFiniteKernel (κ.singularPart η)
have refine : ∀ (a : α), (((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
Tactic: refine ⟨κ.bound, κ.bound_lt_top, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
| ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : ((((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ :
  ℝ≥0∞)
Tactic: rw [← rnDeriv_add_singularPart κ η]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have conv_rhs : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
  (((η.withDensity (κ.rnDeriv η) + κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
Tactic: conv_rhs => rw [← rnDeriv_add_singularPart κ η]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst : IsFiniteKernel η
a : α
⊢ (((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ ≤ κ.bound
have h : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) =
  (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
Tactic: have h : withDensity η (rnDeriv κ η) a univ + singularPart κ η a univ = κ a univ := by
    conv_rhs => rw [← rnDeriv_add_singularPart κ η]
    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 η
⊢ Measurable.{u_1, u_2} (β := Measure γ) fun (a : α) ↦
    Measure.singularPart ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
have refine : ∀ (s : Set γ) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.singularPart ((κ : (a : α) → Measure γ) b) ((η : (a : α) → Measure γ) b) : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s
Tactic: refine Measure.measurable_of_measurable_coe _ (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 η
s : Set γ
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.singularPart ((κ : (a : α) → Measure γ) b) ((η : (a : α) → Measure γ) b) : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦
  ((((κ + η).withDensity fun (a : α) (x : γ) ↦
              (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) -
                (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) * κ.rnDeriv η a x :
            (a : α) → Measure γ)
          b :
        Measure γ) :
      (a : Set γ) → ℝ≥0∞)
    s
Tactic: simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]
-- 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 : α
⊢ (κ.singularPart ν).rnDeriv ν a =ᶠ[ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)] 0
have h : ∀ (x : γ)
  (h1 :
    (κ.singularPart ν).rnDeriv ν a x =
      Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x)
  (h2 : Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x = 0 x),
  (κ.singularPart ν).rnDeriv ν a x = 0 x
Tactic: filter_upwards [(singularPart κ ν).rnDeriv_eq_rnDeriv_measure,
    (Measure.rnDeriv_eq_zero _ _).mpr (mutuallySingular_singularPart κ ν a)] with x h1 h2
-- 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 : α
x : γ
h1 :
  (κ.singularPart ν).rnDeriv ν a x =
    Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x
h2 h : Measure.rnDeriv (m := mγ) ((κ.singularPart ν : (a : α) → Measure γ) a) ((ν : (a : α) → Measure γ) a) x = 0 x
⊢ (κ.singularPart ν).rnDeriv ν a x = 0 x
have h₁ : Eq (α := ℝ≥0∞) (0 x) (0 x)
Tactic: rw [h1, h2]
-- 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 : α
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x < ∞
have h : ∀ (a_1 : γ),
  Membership.mem (γ := Set γ)
    {x : γ |
      Membership.mem (γ := Set γ)
          {x : γ |
            (fun (x : γ) ↦
                κ.rnDeriv η a x =
                  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
              x}
          x →
        Membership.mem (γ := Set γ)
          {x : γ |
            Membership.mem (γ := Set γ)
                {x : γ |
                  (fun (x : γ) ↦
                      Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≠ ∞)
                    x}
                x →
              Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x}
          x}
    a_1
Tactic: filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _]
    with x heq htop using heq ▸ htop.lt_top
-- 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 :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  κ.rnDeriv η a x =
                    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                x}
            x →
          Membership.mem (γ := Set γ)
            {x : γ |
              Membership.mem (γ := Set γ)
                  {x : γ |
                    (fun (x : γ) ↦
                        Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x ≠ ∞)
                      x}
                  x →
                Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x}
            x}
      a_1
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x < ∞
have h₁ : ∀ (a_1 : γ),
  κ.rnDeriv η a a_1 = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) a_1 →
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) a_1 ≠ ∞ →
      κ.rnDeriv η a a_1 < ∞
Tactic: filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _]
    with x heq htop using heq ▸ htop.lt_top
-- 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 : α
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x ≠ ∞
have h : ∀ (a_1 : γ),
  Membership.mem (γ := Set γ)
    {x : γ |
      Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x →
        Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x ≠ ∞) x} x}
    a_1
Tactic: filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne
-- 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 :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x < ∞) x} x →
          Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ κ.rnDeriv η a x ≠ ∞) x} x}
      a_1
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a x ≠ ∞
have h₁ : ∀ (a_1 : γ), κ.rnDeriv η a a_1 < ∞ → κ.rnDeriv η a a_1 ≠ ∞
Tactic: filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
ha : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : γ) ∂((κ : (a : α) → Measure γ) a : Measure γ), 0 < κ.rnDeriv η a x
have h : ∀ (a_1 : γ),
  Membership.mem (γ := Set γ)
    {x : γ |
      Membership.mem (γ := Set γ)
          {x : γ |
            (fun (x : γ) ↦
                κ.rnDeriv η a x =
                  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
              x}
          x →
        Membership.mem (γ := Set γ)
          {x : γ |
            Membership.mem (γ := Set γ)
                {x : γ |
                  (fun (x : γ) ↦
                      0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                    x}
                x →
              Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ 0 < κ.rnDeriv η a x) x} x}
          x}
    a_1
Tactic: filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha]
    with x heq hpos using heq ▸ hpos
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
ha : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  κ.rnDeriv η a x =
                    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                x}
            x →
          Membership.mem (γ := Set γ)
            {x : γ |
              Membership.mem (γ := Set γ)
                  {x : γ |
                    (fun (x : γ) ↦
                        0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x)
                      x}
                  x →
                Membership.mem (γ := Set γ) {x : γ | (fun (x : γ) ↦ 0 < κ.rnDeriv η a x) x} x}
            x}
      a_1
⊢ ∀ᵐ (x : γ) ∂((κ : (a : α) → Measure γ) a : Measure γ), 0 < κ.rnDeriv η a x
have h₁ : ∀ (a_1 : γ),
  κ.rnDeriv η a a_1 = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) a_1 →
    0 < Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) a_1 →
      0 < κ.rnDeriv η a a_1
Tactic: filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha]
    with x heq hpos using heq ▸ hpos
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : γ) ∂((κ : (a : α) → Measure γ) a : Measure γ), 0 < (κ.rnDeriv η a x).toReal
have h₁ : ∀ (x : γ) (h0 : 0 < κ.rnDeriv η a x) (htop : κ.rnDeriv η a x ≠ ∞), 0 < (κ.rnDeriv η a x).toReal
Tactic: filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop