awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑(s i) : ℝ) (↑(s j) : ℝ)

Tactic:
mod_cast hs_mono hij

Premises used: cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑(s i) : ℝ) (↑(s j) : ℝ)

Tactic:
exact mod_cast hs_mono hij
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Monotone s'

Tactic:
exact fun i j hij ↦ Iic_subset_Iic.mpr (by exact mod_cast hs_mono hij)

Premises used: Iff.mpr, Set.Iic_subset_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_2 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (⋃ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) univ x
⊢ Eq (α := Set ℝ) (⋃ (i : ℕ), s' i) univ

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 : ∃ (i : ℕ), x ∈ s' i
⊢ Membership.mem (γ := Set ℝ) (⋃ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) univ x

Tactic:
simp only [mem_iUnion, mem_univ, iff_true]

Premises used: Set.mem_iUnion, iff_true, Set.mem_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 :
  ∀ (hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a),
    let s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ);
    ∀ (x : ℝ), ∃ (i : ℕ), x ∈ s' i
⊢ ∃ (i : ℕ), x ∈ s' i

Tactic:
rw [tendsto_atTop_atTop] at hs_tendsto

Premises used: Filter.tendsto_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 : ∀ (q : ℚ) (hq : x < (↑q : ℝ)), ∃ (i : ℕ), x ∈ s' i
⊢ ∃ (i : ℕ), x ∈ s' i

Tactic:
have ⟨q, hq⟩ := exists_rat_gt x
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
refine_2 : ∀ (i : ℕ) (hi : ∀ (a : ℕ), i ≤ a → q ≤ s a), ∃ (i : ℕ), x ∈ s' i
⊢ ∃ (i : ℕ), x ∈ s' i

Tactic:
obtain ⟨i, hi⟩ := hs_tendsto q
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ ∃ (i : ℕ), x ∈ s' i

Tactic:
⟨i, hq.le.trans ?_⟩

Premises used: LT.lt.le, Exists.intro, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
refine_2 : LE.le (α := ℝ) (↑q : ℝ) (↑(s i) : ℝ)
⊢ ∃ (i : ℕ), x ∈ s' i

Tactic:
refine ⟨i, hq.le.trans ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ LE.le (α := ℝ) (↑q : ℝ) (↑(s i) : ℝ)

Tactic:
mod_cast hi i le_rfl

Premises used: le_rfl, cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : x < (↑q : ℝ)
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → q ≤ s a
⊢ LE.le (α := ℝ) (↑q : ℝ) (↑(s i) : ℝ)

Tactic:
exact mod_cast hi i le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
⊢ IsRatCondKernelCDF (fun (p : α × γ) (q : ℚ) ↦ κ.density κ.fst p.1 p.2 (Iic (↑q : ℝ))) κ κ.fst

Tactic:
(isRatCondKernelCDFAux_density_Iic κ).isRatCondKernelCDF

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF, ProbabilityTheory.Kernel.isRatCondKernelCDFAux_density_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
⊢ IsCondKernelCDF κ.condKernelCDF κ κ.fst

Tactic:
isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_density_Iic κ)

Premises used: ProbabilityTheory.Kernel.condKernelCDF, ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat, ProbabilityTheory.Kernel.isRatCondKernelCDF_density_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel (IsCondKernelCDF.toKernel κ.condKernelCDF ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ IsCondKernelCDF.toKernel κ.condKernelCDF ⋯ = κ
rw₁ rw₂ : κ = κ
⊢ κ.fst ⊗ₖ κ.condKernelReal = κ

Tactic:
rw [condKernelReal, compProd_toKernel]

Premises used: ProbabilityTheory.Kernel.condKernelReal, ProbabilityTheory.compProd_toKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel
    (IsCondKernelCDF.toKernel (fun (p : Unit × α) ↦ condCDF (mα := mα) ((κ : (a : Unit) → Measure (α × ℝ)) ()) p.2) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
rw : const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) = κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitReal = κ

Tactic:
rw [condKernelUnitReal, compProd_toKernel]

Premises used: ProbabilityTheory.compProd_toKernel, ProbabilityTheory.Kernel.condKernelUnitReal
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
h :
  ∀ (a : Unit) (s : Set (α × ℝ)),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) :
              (a : Set (α × ℝ)) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((κ : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) = κ

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
a : Unit
s : Set (α × ℝ)
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) :
          (a : Set (α × ℝ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
simp :
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Membership.mem (γ := Set α)
            (preimage (β := ℝ≥0∞)
              (fun (a : α) ↦
                (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
              {0})
            a then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))

Tactic:
simp only [mem_preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
pos :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞) →
    Eq (α := Measure Ω) (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
      (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
neg :
  ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞) →
    Eq (α := Measure Ω)
      (Measure.comap (embeddingReal Ω)
        (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
      (Measure.comap (embeddingReal Ω)
        (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
h :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := Measure Ω) (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
    (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
h :
  ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
⊢ MeasurableEmbedding (embeddingReal Ω)

Tactic:
have he := measurableEmbedding_embeddingReal Ω
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
rw :
  Eq (α := ℝ≥0∞)
    (((if
                Eq (α := ℝ≥0∞)
                  ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
                  (0 : ℝ≥0∞) then
              Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
            else
              Measure.comap (embeddingReal Ω)
                (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)

Tactic:
rw [borelMarkovFromReal_apply]

Premises used: ProbabilityTheory.Kernel.borelMarkovFromReal_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
pos :
  ∀
    (h :
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      (((Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
neg :
  ∀
    (h :
      ¬Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      (((Measure.comap (embeddingReal Ω)
                (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
              Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((if
                Eq (α := ℝ≥0∞)
                  ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
                  (0 : ℝ≥0∞) then
              Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
            else
              Measure.comap (embeddingReal Ω)
                (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
pos pos₁ :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
    ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs]

Premises used: MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.comap_apply, MeasurableEmbedding.injective
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h :
  ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  Eq (α := ℝ≥0∞)
    ((Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' s) :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)
neg₁ neg₂ :
  Eq (α := ℝ≥0∞) ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯))
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯))
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω)
              (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]

Premises used: MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.comap_apply, MeasurableEmbedding.injective, MeasureTheory.Measure.dirac_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
η : Kernel α ℝ
inst_3 : IsSFiniteKernel η
⊢ IsSFiniteKernel (mβ := mΩ) (borelMarkovFromReal Ω η)

Tactic:
IsSFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω)

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.Kernel.borelMarkovFromReal, ProbabilityTheory.Kernel.IsSFiniteKernel.comapRight
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
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 Ω
η : Kernel α ℝ
inst_3 : IsFiniteKernel η
⊢ IsFiniteKernel (mβ := mΩ) (borelMarkovFromReal Ω η)

Tactic:
IsFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω)

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, ProbabilityTheory.Kernel.borelMarkovFromReal, ProbabilityTheory.Kernel.IsFiniteKernel.comapRight