awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ (ae (F := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) t)).EventuallyLE (β := ENNReal)
    (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) fun (b : β) ↦ 1

Tactic:
ae_of_all _ fun b ↦ ?_

Premises used: MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
h_le :
  ∀ (b : β),
    LE.le (α := ENNReal)
      ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
      ((fun (b : β) ↦ (1 : ENNReal)) b)
⊢ (ae (F := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) t)).EventuallyLE (β := ENNReal)
    (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) fun (b : β) ↦ 1

Tactic:
refine ae_of_all _ fun b ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
b : β
h_le :
  LE.le (α := ENNReal)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (b_1 : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)) b)
⊢ LE.le (α := ENNReal)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (b : β) ↦ (1 : ENNReal)) b)

Tactic:
rw [← measure_univ (μ := η b)]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
b : β
⊢ s ⊆ univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
b : β
⊢ LE.le (α := ENNReal)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (b_1 : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)) b)

Tactic:
exact measure_mono (by simp)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (b : β),
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a

Tactic:
setLIntegral_le_lintegral _ _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
e_f :
  ∀ (x : β),
    HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ
⊢ ∫⁻ (b : β),
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a

Tactic:
congr with x
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
x : β
⊢ Ne (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
x : β
e_f :
  HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
    HSub.hSub (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
⊢ HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
    (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ

Tactic:
rw [measure_compl hs (by simp)]

Premises used: MeasureTheory.measure_compl
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
x : β
⊢ HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
    HSub.hSub (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)
      ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
rw rw₁ :
  ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a =
    (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ

Tactic:
rw [η.comp_apply' _ _ hs.compl]

Premises used: MeasurableSet.compl, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
⊢ Ne (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
rw :
  HSub.hSub (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
    0
rw₁ :
  HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
    0
rw₂ : HSub.hSub (α := ENNReal) 1 1 = 0
rw₃ rw₄ : Eq (α := ENNReal) 0 0
⊢ Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal)
    (0 : ENNReal)

Tactic:
rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]

Premises used: MeasureTheory.measure_compl, MeasureTheory.IsZeroOneMeasure.measure_univ, tsub_self
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
⊢ ρ.fst ⊗ₘ ρCond = ρ

Tactic:
IsCondKernel.disintegrate

Premises used: MeasureTheory.Measure.IsCondKernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
hρ : ρ ≠ 0
contrapose : ∀ (hρ : ¬IsSFiniteKernel ρCond), ρ = 0
⊢ IsSFiniteKernel ρCond

Tactic:
contrapose hρ
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
rwa : ρ.fst ⊗ₘ ρCond = 0
rwa₁ : Eq (α := Measure (α × Ω)) 0 0
h : ¬IsSFiniteKernel ρCond
rwa₂ : Eq (α := Measure (α × Ω)) 0 0
h₁ h₂ h₃ : ¬IsSFiniteKernel ρCond
⊢ ρ = 0

Tactic:
rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel]

Premises used: MeasureTheory.Measure.disintegrate, MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρCond : Kernel α Ω
inst : MeasurableSingletonClass α
x : α
s : Set Ω
hs : MeasurableSet s
inst_1 : IsCondKernel 0 ρCond
inst_2 : IsFiniteMeasure (α := α × Ω) (m0 := Prod.instMeasurableSpace) 0
hx : Ne (α := ℝ≥0∞) (((fst.{u_1, u_3} (β := Ω) 0 : Measure α) : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
⊢ IsSFiniteKernel ρCond

Tactic:
have := isSFiniteKernel ρ ρCond (by rintro rfl; simp at hx)
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
nth_rewrite :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((ρ.fst ⊗ₘ ρCond : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)

Tactic:
nth_rewrite 2 [← ρ.disintegrate ρCond]

Premises used: MeasureTheory.Measure.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
rw :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α),
        (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) ∂ρ.fst)
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((ρ.fst ⊗ₘ ρCond : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)

Tactic:
rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))]

Premises used: Iff.mpr, MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.compProd_apply, And.intro, Or.inl, measurableSet_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
inl :
  ∀ (hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {a} s) :
        ℝ≥0∞)
      (indicator {a} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
inr :
  ∀ (hax : a ≠ x),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
      ℝ≥0∞)
    (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)

Tactic:
obtain rfl | hax := eq_or_ne a x

Premises used: eq_or_ne, rfl