awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
rw :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) univ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
have rw₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
Tactic: rw [← setIntegral_univ, setIntegral_density_of_measurableSet hκν 0 a hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
have this : IsFiniteKernel κ
Tactic: have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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}
have rw : mγ = generateFrom (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
Tactic: rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 κ
rw : mγ = generateFrom (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
⊢ mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
have rw₁ : mγ = ⨆ (n : ℕ), (↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n
Tactic: rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 κ
rw : mγ = generateFrom (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
rw₁ : mγ = ⨆ (n : ℕ), (↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n
⊢ mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
have rw₂ : mγ = mγ
Tactic: rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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 κ
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
have hgen : 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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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}
have rw : IsPiSystem.{u_3} (α := γ) (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
Tactic: rw [setOf_exists]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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}
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
have hpi : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
⊢ (@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)
have 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)
Tactic: rcases hs with ⟨n, hn⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)
have 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
Tactic: have h := integral_add_compl hA (integrable_density hκν a hs)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)
have 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)
Tactic: rw [hA_eq, integral_density hκν a hs] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
have rw : (univ \ A) ×ˢ s = SProd.sprod (α := Set γ) univ (s \ s) ∪ (univ \ A) ×ˢ s
Tactic: rw [prod_diff_prod, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (Aᶜ ×ˢ s)
have 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))
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 _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
⊢ (@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))
have 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))
Tactic: rw [eq_tsub_iff_add_eq_of_le, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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))
⊢ (@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))
have 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))
Tactic: rw [eq_tsub_iff_add_eq_of_le, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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)) ≤
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))
have compl : Ne (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set γ) univ s) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 :
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ 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))
have compl₁ : A ⊆ univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : ℕ), f i)) fun (x : γ) ↦
      κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)
have iUnion : (∑' (n : ℕ),
    @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f n)) fun (x : γ) ↦ κ.density ν a x s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
    (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)
Tactic: rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]