awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
have hg : Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s
Tactic: rw [lintegral_sub]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
hg : Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s
⊢ ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
have hg_fin : ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≠ ⊤
Tactic: rw [lintegral_sub]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
hg : Measurable (β := ENNReal) fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s
hg_fin :
  ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≠
    ⊤
⊢ ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
have h_le : (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: rw [lintegral_sub]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
have h_le : ∀ (b : β),
  LE.le (α := ENNReal)
    ((fun (b : β) ↦ ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)) b)
    ((fun (b : β) ↦ (1 : ENNReal)) b)
Tactic: refine ae_of_all _ fun b ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 : ENNReal)) b)
have 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)
Tactic: rw [← measure_univ (μ := η b)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 : β),
      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
have 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ᶜ
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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) =
    (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ
have 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)
Tactic: rw [measure_compl hs (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a =
    (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ
have 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
Tactic: rw [η.comp_apply' _ _ hs.compl]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal)
    (0 : ENNReal)
have rw : HSub.hSub (α := ENNReal) (β := ENNReal)
    ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) univ : ENNReal)
    ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
  0
Tactic: rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal)
    (0 : ENNReal)
have rw₁ : HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
    ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) =
  0
Tactic: rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal)
    (0 : ENNReal)
have rw₂ : HSub.hSub (α := ENNReal) 1 1 = 0
Tactic: rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) sᶜ : ENNReal)
    (0 : ENNReal)
have rw₃ : Eq (α := ENNReal) 0 0
Tactic: rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) ≤
    0
have _ : HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
    (∫⁻ (a : β) in t,
      (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
  ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
    ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a
Tactic: calc
    _ = ∫⁻ b in t, 1 ∂κ a - ∫⁻ b in t, (η b) s ∂κ a := by
      rw [setLIntegral_one]
    _ = ∫⁻ b in t, 1 - (η b) s ∂κ a := by
      rw [lintegral_sub]
      · exact η.measurable_coe hs
      · exact ne_top_of_le_ne_top (by simp) integral_le_kernel
      · refine ae_of_all _ fun b ↦ ?_
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
    _ ≤ ∫⁻ b, 1 - (η b) s ∂κ a := setLIntegral_le_lintegral _ _
    _ = ∫⁻ x, (η x) sᶜ ∂κ a := by
        congr with x
        rw [measure_compl hs (by simp)]
        simp
    _ = (η ∘ₖ κ) a sᶜ := by
        rw [η.comp_apply' _ _ hs.compl]
    _ = 0 := by
      rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
_ :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) ≤
    0
have _₁ : ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
    ∫⁻ (b : β) in t,
      (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β) in t,
    HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
Tactic: calc
    _ = ∫⁻ b in t, 1 ∂κ a - ∫⁻ b in t, (η b) s ∂κ a := by
      rw [setLIntegral_one]
    _ = ∫⁻ b in t, 1 - (η b) s ∂κ a := by
      rw [lintegral_sub]
      · exact η.measurable_coe hs
      · exact ne_top_of_le_ne_top (by simp) integral_le_kernel
      · refine ae_of_all _ fun b ↦ ?_
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
    _ ≤ ∫⁻ b, 1 - (η b) s ∂κ a := setLIntegral_le_lintegral _ _
    _ = ∫⁻ x, (η x) sᶜ ∂κ a := by
        congr with x
        rw [measure_compl hs (by simp)]
        simp
    _ = (η ∘ₖ κ) a sᶜ := by
        rw [η.comp_apply' _ _ hs.compl]
    _ = 0 := by
      rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]