awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
pos :
  ∀ (hα : Countable α),
    κ.fst ⊗ₖ condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯ = κ
⊢ (κ.fst ⊗ₖ
      if hα : Countable α then
        condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
      else κ.condKernelBorel) =
    κ
have neg : ∀ (hα : ¬Countable α), κ.fst ⊗ₖ κ.condKernelBorel = κ
Tactic: split_ifs with hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have refine : ∀ (t : Set α) (ht : MeasurableSet t),
  LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
      ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
    (Kernel.measurable_coe κ hs) (Kernel.measurable_coe ρ.condKernel hs) (fun t ht _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
| ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst
have rw : ((ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s) : ℝ≥0∞)
Tactic: rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
    ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst
have conv_rhs : ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
  (ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s)
Tactic: conv_rhs => rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
have huniv : ∀ᵐ (x : α) ∂ρ.fst,
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have huniv : ∀ᵐ x ∂ρ.fst, κ x Set.univ = ρ.condKernel x Set.univ :=
    eq_condKernel_of_measure_eq_compProd' κ hκ MeasurableSet.univ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
this :
  ∀ᵐ (x : α) ∂ρ.fst,
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
have h : ∀ (x : α)
  (hx :
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)),
  Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
have suffices : ∀ᵐ (x : α) ∂ρ.fst,
  ∀ ⦃t : Set ℝ⦄,
    MeasurableSet t →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
        ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: suffices ∀ᵐ x ∂ρ.fst, ∀ ⦃t⦄, MeasurableSet t → κ x t = ρ.condKernel x t by
    filter_upwards [this] with x hx
    ext t ht; exact hx ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
have h_empty : ∀ᵐ (x : α) ∂ρ.fst,
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
h_empty :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
have h_basic : ∀ᵐ (x : α) ∂ρ.fst,
  ∀ (t : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) t →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
        ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
h_empty :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
h_basic :
  ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (t : Set ℝ),
      Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
have h_compl : ∀ᵐ (x : α) ∂ρ.fst,
  ∀ (t : Set ℝ),
    MeasurableSet t →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
h_empty :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
h_basic :
  ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (t : Set ℝ),
      Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
h_compl :
  ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (t : Set ℝ),
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
            ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
            ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ ⦃t : Set ℝ⦄,
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
have h_union : ∀ᵐ (x : α) ∂ρ.fst,
  ∀ (f : ℕ → Set ℝ),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
              ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)) →
          Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (t : Set ℝ),
      Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), {Iic (↑a : ℝ)}) t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
have h_basic : ∀ᵐ (x : α) ∂ρ.fst,
  ∀ (a : ℚ),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑a : ℝ)) : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑a : ℝ)) : ℝ≥0∞)
Tactic: simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (t : Set ℝ),
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
            ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
            ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h : ∀ (x : α)
  (hxuniv :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞))
  (t : Set ℝ) (ht : MeasurableSet t)
  (heq :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: filter_upwards [huniv] with x hxuniv t ht heq
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
x : α
hxuniv :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
t : Set ℝ
ht : MeasurableSet t
heq :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
  (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
Tactic: rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
x : α
hxuniv :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
t : Set ℝ
ht : MeasurableSet t
heq :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
  (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
Tactic: rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
x : α
hxuniv :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
t : Set ℝ
ht : MeasurableSet t
heq :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
h₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
  (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
Tactic: rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
x : α
hxuniv :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
t : Set ℝ
ht : MeasurableSet t
heq :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
h₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
h₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
    (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₃ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]