awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
f : (a : α) → β
hf :
  ∀ (a : α), Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)
s : Set β
hs : MeasurableSet s
this :
  f ⁻¹' s =
    preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1}
⊢ MeasurableSet.{u_1} (α := α)
    (preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1})

Tactic:
κ.measurable_coe hs <| measurableSet_singleton 1

Premises used: MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.Kernel.measurable_coe, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
f : (a : α) → β
hf :
  ∀ (a : α), Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)
s : Set β
hs : MeasurableSet s
this :
  f ⁻¹' s =
    preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1}
⊢ MeasurableSet.{u_1} (α := α)
    (preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1})

Tactic:
exact κ.measurable_coe hs <| measurableSet_singleton 1

Premises used: MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.Kernel.measurable_coe, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
f : (a : α) → β
hf :
  ∀ (a : α), Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)
refine_2 :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      (((deterministic f ⋯ : Kernel α β) : (a : α) → Measure β) a : Measure β)
⊢ κ = deterministic f ⋯

Tactic:
ext a : 1
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
f : (a : α) → β
hf :
  ∀ (a : α), Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (((deterministic f ⋯ : Kernel α β) : (a : α) → Measure β) a : Measure β)

Tactic:
hf a

Premises used: MeasureTheory.Measure.dirac, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
f : (a : α) → β
hf :
  ∀ (a : α), Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (((deterministic f ⋯ : Kernel α β) : (a : α) → Measure β) a : Measure β)

Tactic:
exact hf a
-- 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 (η ∘ₖ κ)
h :
  ∀ (a : α),
    Eq (α := Measure (γ × β)) ((η ∘ₖ κ ×ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
      ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
⊢ η ∘ₖ κ ×ₖ κ = η ×ₖ Kernel.id ∘ₖ κ

Tactic:
ext a : 1
-- 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 : α
h :
  Eq (α := Measure (γ × β)) (Measure.prod ((η ∘ₖ κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure β) a))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a)
⊢ Eq (α := Measure (γ × β)) ((η ∘ₖ κ ×ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))

Tactic:
rw [prod_apply]

Premises used: ProbabilityTheory.Kernel.prod_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 : α
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((η ∘ₖ κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure β) a))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a)

Tactic:
Measure.prod_eq fun s t hs ht ↦ ?_

Premises used: MeasureTheory.Measure.prod_eq
-- 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 : α
h :
  ∀ (s : Set γ) (t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
    (((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ENNReal) (s ×ˢ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((η ∘ₖ κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure β) a))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a)

Tactic:
refine Measure.prod_eq fun s t hs ht ↦ ?_

Premises used: MeasureTheory.Measure.prod_eq
-- 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
h :
  ∫⁻ (b : β),
      (((η ×ₖ Kernel.id : (a : β) → Measure (γ × β)) b : Measure (γ × β)) : (a : Set (γ × β)) → ENNReal)
        (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ (((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ENNReal) (s ×ˢ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
rw [comp_apply' _ _ _ (hs.prod ht)]

Premises used: MeasurableSet.prod, 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
h :
  ∫⁻ (b : β),
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (t.indicator 1 b : ENNReal) ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ ∫⁻ (b : β),
      (((η ×ₖ Kernel.id : (a : β) → Measure (γ × β)) b : Measure (γ × β)) : (a : Set (γ × β)) → ENNReal)
        (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
simp_rw [prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ ht]

Premises used: MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.prod_apply_prod
-- 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
b : β
pos :
  b ∈ t →
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 b : ENNReal) =
      (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s
neg :
  b ∉ t →
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal) =
      0
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      (if b ∈ t then 1 b else 0 : ENNReal) =
    if b ∈ t then (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s else 0

Tactic:
split_ifs
-- 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
b : β
h : b ∈ t
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 b : ENNReal) =
    (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s

Tactic:
simp_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
b : β
h : b ∉ t
⊢ HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal) =
    0

Tactic:
simp_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
⊢ ∀ (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

Tactic:
have (b : β) : (η b) s * t.indicator 1 b = t.indicator (fun b ↦ η b s) b := by
    simp only [indicator]
    split_ifs
    all_goals simp_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 :
  ∫⁻ (b : β),
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s)
        b ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ ∫⁻ (b : β),
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (t.indicator 1 b : ENNReal) ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
simp_rw [this]
-- 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 :
  ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ ∫⁻ (b : β),
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s)
        b ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
rw [lintegral_indicator ht]

Premises used: MeasureTheory.lintegral_indicator
-- 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 :
  ∀
    (h₀ :
      Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (0 : ENNReal)),
    ∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
h₁ :
  ∀
    (h₁ :
      Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (1 : ENNReal)),
    ∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
rcases ((η ∘ₖ κ) a).zero_one s with (h₀ | h₁)

Premises used: ProbabilityTheory.Kernel.comp, MeasureTheory.Measure.zero_one, DFunLike.coe
-- 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) (0 : ENNReal)
h :
  ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ ∫⁻ (a : β) in t, (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)

Tactic:
rw [h₀, zero_mul, setLIntegral_eq_zero_iff ht <| η.measurable_coe hs]

Premises used: MulZeroClass.zero_mul, MeasureTheory.setLIntegral_eq_zero_iff, ProbabilityTheory.Kernel.measurable_coe
-- 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) (0 : ENNReal)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0

Tactic:
rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff <| η.measurable_coe hs] at h₀

Premises used: MeasureTheory.lintegral_eq_zero_iff, ProbabilityTheory.Kernel.measurable_coe, 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₀ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
x : β
hx : Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 x : ENNReal)
h :
  x ∈ t →
    Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ x ∈ t →
    Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
_
-- 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₀ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
x : β
hx : Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 x : ENNReal)
h : x ∈ t
⊢ Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
hx
-- 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₀ :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ENNReal)
    (fun (a : β) ↦ (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s) 0
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ENNReal)
                    ((fun (a : β) ↦ ((((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal))
                      x)
                    (0 x))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  x ∈ t →
                    Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
                      (0 : ENNReal))
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : β)
    (hx :
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal)
        (0 x : ENNReal)),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ ∀ᵐ (x : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    x ∈ t →
      Eq (α := ENNReal) ((((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
filter_upwards [h₀] with x hx _ using hx