awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
h₁ :
  ∀ (b : β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b)) ↔
      Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))

Tactic:
convert! this with b
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
b : β
⊢ IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b)) ↔
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, Iff.intro, MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
b : β
⊢ IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b)) ↔
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
pos :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))

Tactic:
suffices ∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ = 1 by
    convert! this with b
    exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
b : β
h1 :
  LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
h2 :
  LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
le_antisymm h1 h2

Premises used: le_antisymm
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LE.le (α := ℝ≥0∞)
                    ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                    (1 : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β)
                  {x : β |
                    (fun (b : β) ↦
                        LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
                          ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞))
                      x}
                  x →
                Membership.mem (γ := Set β)
                  {x : β |
                    (fun (b : β) ↦
                        Eq (α := ℝ≥0∞)
                          ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                          (1 : ℝ≥0∞))
                      x}
                  x}
            x}
      a_1
h₂ h₃ :
  ∀ (b : β)
    (h1 :
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞))
    (h2 :
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
pos :
  (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
suffices (∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ ≤ 1)
      ∧ (∀ᵐ b ∂(κ.fst a), 1 ≤ κCond (a, b) Set.univ) by
    filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
rw : (((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
| ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← h]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
conv_rhs :
  ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    ((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
conv_rhs => rw [← h]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
rw rw₁ :
  ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a
⊢ ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    ((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [fst_compProd_apply _ _ _ hs]

Premises used: ProbabilityTheory.Kernel.fst_compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
⊢ ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
have h_eq s (hs : MeasurableSet s) :
      ∫⁻ b, s.indicator (fun b ↦ κCond (a, b) Set.univ) b ∂κ.fst a = κ.fst a s := by
    conv_rhs => rw [← h]
    rw [fst_compProd_apply _ _ _ hs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ

Tactic:
have h_meas : Measurable fun b ↦ κCond (a, b) Set.univ :=
    (κCond.measurable_coe MeasurableSet.univ).comp measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
pos :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
pos₁ :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
pos :
  ∀ (b : ℝ≥0∞),
    1 < b →
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
            {x : β | b ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
rw [ae_le_const_iff_forall_gt_measure_zero]

Premises used: MeasureTheory.ae_le_const_iff_forall_gt_measure_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet s := h_meas measurableSet_Ici
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
b : β
pos :
  ∀ (hbs : b ∈ s),
    LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
      (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
neg :
  ∀ (hbs : b ∉ s),
    LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
      (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)

Tactic:
by_cases hbs : b ∈ s
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
b : β
hbs : b ∈ s
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)

Tactic:
simpa [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)

Tactic:
simp [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
⊢ LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)

Tactic:
have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) := by
      intro b
      by_cases hbs : b ∈ s
      · simpa [hbs]
      · simp [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
⊢ ∫⁻ (b : β), s.indicator (fun (x : β) ↦ r) b ∂(κ.fst : (a : α) → Measure β) a ≤
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
      (lintegral_mono h_2_le).trans_eq (h_eq s hs)