awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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∞)
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 ℝ)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
hx h :
  ∀ (t : Set ℝ) (ht : 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:
ext t ht
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
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∞)
t : Set ℝ
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hx ht
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
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∞)
t : Set ℝ
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact hx ht
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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∞)
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∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) ((κ : (a : α) → Measure ℝ) x : Measure ℝ) ((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

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
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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∞)
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∞)
⊢ ∀ᵐ (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:
apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat

Premises used: Real.isPiSystem_Iic_rat, MeasurableSpace.ae_induction_on_inter, Real.borel_eq_generateFrom_Iic_rat
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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_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∞)
⊢ ∀ᵐ (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:
simp only [iUnion_singleton_eq_range, mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, Set.iUnion_singleton_eq_range, forall_apply_eq_imp_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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,
    ∀ (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:
ae_all_iff.2 fun q ↦ eq_condKernel_of_measure_eq_compProd' κ hκ measurableSet_Iic

Premises used: Iff.mpr, measurableSet_Iic, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd', MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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,
    ∀ (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:
exact ae_all_iff.2 fun q ↦ eq_condKernel_of_measure_eq_compProd' κ hκ measurableSet_Iic

Premises used: Iff.mpr, measurableSet_Iic, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd', MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 :
  ∀ (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∞)
⊢ ∀ᵐ (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:
filter_upwards [huniv] with x hxuniv t ht heq
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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ᶜ
h₃ 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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) tᶜ : ℝ≥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 _ _]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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,
    ∀ (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:
ae_of_all _ (fun x f hdisj hf heq ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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_union :
  ∀ (x : α) (f : ℕ → Set ℝ) (hdisj : Pairwise (Function.onFun Disjoint f)) (hf : ∀ (i : ℕ), MeasurableSet (f i))
    (heq :
      ∀ (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∞)
⊢ ∀ᵐ (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:
refine ae_of_all _ (fun x f hdisj hf heq ↦ ?_)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
h_union :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), (((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
    (∑' (i : ℕ), (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
⊢ 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:
rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (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∞) (∑' (i : ℕ), (((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
    (∑' (i : ℕ), (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))

Tactic:
tsum_congr heq

Premises used: tsum_congr
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (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∞) (∑' (i : ℕ), (((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
    (∑' (i : ℕ), (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))

Tactic:
exact tsum_congr heq

Premises used: tsum_congr
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
⊢ MeasurableEmbedding (embeddingReal Ω)

Tactic:
have hf := measurableEmbedding_embeddingReal Ω
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
⊢ let ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ;
  ρ' = Measure.map (Prod.map id f) ρ

Tactic:
set ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) with hρ'def

Premises used: Real, MeasureTheory.Measure, id, Prod.map, MeasureTheory.Measure.map, Prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ρ'.fst = ρ.fst

Tactic:
ext s hs