awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}

Tactic:
have hgen : ‹MeasurableSpace γ› =
      .generateFrom {s | ∃ n, MeasurableSet[countableFiltration γ n] s} := by
    rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
rw : IsPiSystem.{u_3} (α := γ) (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
⊢ IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}

Tactic:
rw [setOf_exists]

Premises used: Set.setOf_exists
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
⊢ IsPiSystem.{u_3} (α := γ) (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})

Tactic:
isPiSystem_iUnion_of_monotone _
      (fun n ↦ @isPiSystem_measurableSet _ (countableFiltration γ n))
      fun _ _ ↦ (countableFiltration γ).mono

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_iUnion_of_monotone, ProbabilityTheory.countableFiltration, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
⊢ IsPiSystem.{u_3} (α := γ) (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})

Tactic:
exact isPiSystem_iUnion_of_monotone _
      (fun n ↦ @isPiSystem_measurableSet _ (countableFiltration γ n))
      fun _ _ ↦ (countableFiltration γ).mono

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_iUnion_of_monotone, ProbabilityTheory.countableFiltration, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
⊢ IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}

Tactic:
have hpi : IsPiSystem {s | ∃ n, MeasurableSet[countableFiltration γ n] s} := by
    rw [setOf_exists]
    exact isPiSystem_iUnion_of_monotone _
      (fun n ↦ @isPiSystem_measurableSet _ (countableFiltration γ n))
      fun _ _ ↦ (countableFiltration γ).mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) ∅) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) ∅ s)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s_1 : Set β
hs_1 : MeasurableSet s_1
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
s : Set γ
hs : Membership.mem (γ := Set (Set γ)) {s : Set γ | ∃ (n : ℕ), MeasurableSet s} s
basic :
  ∀ (n : ℕ) (hn : MeasurableSet s),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s) fun (x : γ) ↦ κ.density ν a x s_1) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (s ×ˢ s_1)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s) fun (x : γ) ↦ κ.density ν a x s_1) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (s ×ˢ s_1)

Tactic:
rcases hs with ⟨n, hn⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s_1 : Set β
hs : MeasurableSet s_1
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
s : Set γ
n : ℕ
hn : MeasurableSet s
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s) fun (x : γ) ↦ κ.density ν a x s_1) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (s ×ˢ s_1)

Tactic:
setIntegral_density_of_measurableSet hκν n a hs hn

Premises used: ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s_1 : Set β
hs : MeasurableSet s_1
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
s : Set γ
n : ℕ
hn : MeasurableSet s
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s) fun (x : γ) ↦ κ.density ν a x s_1) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (s ×ˢ s_1)

Tactic:
exact setIntegral_density_of_measurableSet hκν n a hs hn

Premises used: ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
⊢ HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x s

Tactic:
have h := integral_add_compl hA (integrable_density hκν a hs)
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x s
⊢ (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)

Tactic:
rw [hA_eq, integral_density hκν a hs] at h

Premises used: ProbabilityTheory.Kernel.integral_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
rw : (univ \ A) ×ˢ s = SProd.sprod (α := Set γ) univ (s \ s) ∪ (univ \ A) ×ˢ s
⊢ Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s

Tactic:
rw [prod_diff_prod, compl_eq_univ_diff]

Premises used: Set.prod_diff_prod, Set.compl_eq_univ_diff
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
⊢ (univ \ A) ×ˢ s = SProd.sprod (α := Set γ) univ (s \ s) ∪ (univ \ A) ×ˢ s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
⊢ Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s

Tactic:
have : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s := by
      rw [prod_diff_prod, compl_eq_univ_diff]
      simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
a_1 : γ × β
⊢ a_1 ∈ A ×ˢ s → a_1 ∈ SProd.sprod (α := Set γ) univ s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
x : γ × β
⊢ x ∈ A ×ˢ s → x ∈ SProd.sprod (α := Set γ) univ s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
compl :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ s)) -
      ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s))
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)

Tactic:
rw [this, measureReal_def,
      measure_diff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),
      ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_ne_top, MeasurableSet.prod, ENNReal.toReal_sub_of_le, MeasureTheory.measure_diff, MeasureTheory.measure_mono, MeasureTheory.measureReal_def, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
compl :
  (ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))
compl₁ :
  ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)) ≤
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ s)) -
      ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s))

Tactic:
rw [eq_tsub_iff_add_eq_of_le, add_comm]

Premises used: add_comm, eq_tsub_iff_add_eq_of_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
⊢ (ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))

Tactic:
h

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
⊢ (ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))

Tactic:
exact h