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 : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
h :
  ∀ (x : γ) (hx_lt : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x < ∞),
    x ∈ s →
      ENNReal.ofReal
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
        Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x
⊢ ∀ᵐ (x : γ) ∂((κ + η : (a : α) → Measure γ) a : Measure γ),
    x ∈ s →
      ENNReal.ofReal
          (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
        Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x

Tactic:
filter_upwards [Measure.rnDeriv_lt_top (κ a) ((κ + η) a)] with x hx_lt _

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, HAdd.hAdd, DFunLike.coe
-- 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a)
    ((κ + η : (a : α) → Measure γ) a)
x : γ
hx_lt : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x < ∞
h_1 : x ∈ s
h h₁ :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x
⊢ ENNReal.ofReal (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x).toReal =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((κ + η : (a : α) → Measure γ) a) x

Tactic:
rw [ENNReal.ofReal_toReal hx_lt.ne]

Premises used: ENNReal.ofReal_toReal, LT.lt.ne
-- 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
⊢ MeasurableSpace.CountablyGenerated γ

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable (β := γ × Unit) fun (a : γ) ↦ (a, ())

Tactic:
fun_prop
-- 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
neg :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (density (β := Unit) (mβ := PUnit.instMeasurableSpace) (κ.map fun (a : γ) ↦ (a, ())) (κ + η) a x
          univ) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
rw [setLIntegral_density ((fst_map_id_prod _ measurable_const).trans_le h_le) _
      MeasurableSet.univ hs, map_apply' _ (by fun_prop) _ (hs.prod MeasurableSet.univ)]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasurableSet.prod, Eq.trans_le, ProbabilityTheory.Kernel.setLIntegral_density, ProbabilityTheory.Kernel.fst_map_id_prod, measurable_const, MeasurableSet.univ
-- 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
neg : ∀ (x : γ), Membership.mem (γ := Set γ) ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) x ↔ x ∈ s
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
congr 1 with x
-- 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 : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
x : γ
⊢ Membership.mem (γ := Set γ) ((fun (a : γ) ↦ (a, ())) ⁻¹' SProd.sprod (β := Set Unit) s univ) x ↔ x ∈ s

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 η
h :
  ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = κ

Tactic:
ext a s hs
-- 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 : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : γ) in s, (↑(κ.rnDerivAux (κ + η) a b).toNNReal : ℝ≥0∞) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
h₁ :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.withDensity_apply']

Premises used: ProbabilityTheory.Kernel.withDensity_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 : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (α := α × γ) (β := ℝ≥0∞)
    (Function.uncurry fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞))

Tactic:
fun_prop
-- 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 : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
setLIntegral_rnDerivAux κ η a hs

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDerivAux
-- 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 : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
exact setLIntegral_rnDerivAux κ η a hs

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDerivAux
-- 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 η
⊢ κ ≤ κ + η

Tactic:
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
-- 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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
h :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                    (a : α) → Measure γ)
                  a :
                Measure γ) :
              (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = η

Tactic:
ext a s
-- 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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
a : α
s : Set γ
h : MeasurableSet s
rw :
  (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
                (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
              (a : α) → Measure γ)
            a :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this]
-- 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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
a : α
s : Set γ
h : MeasurableSet s
⊢ (((κ + η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
a : α
s : Set γ
h : MeasurableSet s
⊢ (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
                (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
              (a : α) → Measure γ)
            a :
          Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      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 η
h_le : κ ≤ κ + η
suffices :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) = η

Tactic:
suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
      + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))
      = κ + η by
    ext a s
    have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      simp
    simp only [coe_add, Pi.add_apply, Measure.coe_add] at h
    rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at 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 η
h_le : κ ≤ κ + η
simp_rw :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η

Tactic:
simp_rw [ofNNReal_toNNReal, ENNReal.ofReal_sub _ (rnDerivAux_nonneg h_le), ENNReal.ofReal_one]

Premises used: ENNReal.ofNNReal_toNNReal, ENNReal.ofReal_one, ProbabilityTheory.Kernel.rnDerivAux_nonneg, ENNReal.ofReal_sub
-- 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 η
h_le : κ ≤ κ + η
rw : ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η
hf : Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)
hg :
  Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))
hfg :
  ∀ (a : α),
    (ae (F := Measure γ) ((κ + η : (a : α) → Measure γ) a : Measure γ)).EventuallyLE (β := ℝ≥0∞)
      (fun (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) fun (x : γ) ↦ 1
⊢ (((κ + η).withDensity fun (a : α) (x : γ) ↦ 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) =
    κ + η

Tactic:
rw [withDensity_sub_add_cancel]

Premises used: ProbabilityTheory.Kernel.withDensity_sub_add_cancel
-- 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 η
h_le : κ ≤ κ + η
rw rw₁ : κ + η = κ + η
⊢ ((κ + η).withDensity fun (a : α) (x : γ) ↦ 1) = κ + η

Tactic:
rw [withDensity_one']

Premises used: ProbabilityTheory.Kernel.withDensity_one'
-- 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 η
h_le : κ ≤ κ + η
⊢ Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)

Tactic:
measurable_const

Premises used: ENNReal.ofNNReal, WithTop.some, measurable_const
-- 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 η
h_le : κ ≤ κ + η
⊢ Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ 1)

Tactic:
exact measurable_const

Premises used: measurable_const
-- 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 η
h_le : κ ≤ κ + η
⊢ Measurable (α := α × γ) (β := ℝ≥0∞) (Function.uncurry fun (a : α) (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))

Tactic:
fun_prop
-- 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 η
h_le : κ ≤ κ + η
a : α
h : ∀ (x : γ) (hx : κ.rnDerivAux (κ + η) a x ≤ 1 x), ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1
⊢ (ae (F := Measure γ) ((κ + η : (a : α) → Measure γ) a : Measure γ)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : γ) ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) fun (x : γ) ↦ 1

Tactic:
filter_upwards [rnDerivAux_le_one h_le] with x hx

Premises used: ProbabilityTheory.Kernel.rnDerivAux_le_one
-- 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 η
h_le : κ ≤ κ + η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
h : κ.rnDerivAux (κ + η) a x ≤ 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ≤ 1

Tactic:
simp only [ENNReal.ofReal_le_one]

Premises used: ENNReal.ofReal_le_one
-- 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 η
h_le : κ ≤ κ + η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ κ.rnDerivAux (κ + η) a x ≤ 1

Tactic:
hx
-- 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 η
h_le : κ ≤ κ + η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x ≤ 1 x
⊢ κ.rnDerivAux (κ + η) a x ≤ 1

Tactic:
exact hx
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
rw : Membership.mem (γ := Set γ) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} x ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
rw₁ rw₂ : 1 ≤ κ.rnDerivAux (κ + η) a x ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
rw [mutuallySingularSetSlice, mem_setOf]

Premises used: Set.mem_setOf, ProbabilityTheory.Kernel.mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∉ κ.mutuallySingularSetSlice η a ↔ κ.rnDerivAux (κ + η) a x < 1

Tactic:
simp [mutuallySingularSetSlice]

Premises used: ProbabilityTheory.Kernel.mutuallySingularSetSlice
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ MeasurableSet (κ.mutuallySingularSet η)

Tactic:
measurable_rnDerivAux κ (κ + η) measurableSet_Ici

Premises used: ProbabilityTheory.Kernel.measurable_rnDerivAux, Set.Mem, setOf, ProbabilityTheory.Kernel.mutuallySingularSet, Set.preimage, HAdd.hAdd, measurableSet_Ici
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ MeasurableSet (κ.mutuallySingularSetSlice η a)

Tactic:
measurable_prodMk_left (measurableSet_mutuallySingularSet κ η)

Premises used: Set.Mem, setOf, ProbabilityTheory.Kernel.mutuallySingularSet, ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet, Set.preimage, ProbabilityTheory.Kernel.mutuallySingularSetSlice, measurable_prodMk_left
-- 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 :
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) {x : γ | 1 ≤ κ.rnDerivAux (κ + η) a x} : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rwa [withDensity_one_sub_rnDerivAux κ η] at this

Premises used: ProbabilityTheory.Kernel.withDensity_one_sub_rnDerivAux