awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
simp_rw : deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
simp_rw₁ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = copy β ∘ₖ deterministic f hf
simp_rw₂ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = deterministic (fun (x : β) ↦ (x, x)) ⋯ ∘ₖ deterministic f hf
simp_rw₃ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = deterministic ((fun (x : β) ↦ (x, x)) ∘ f) ⋯
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf

Tactic:
simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.parallelComp_comp_copy, Function.comp_def, ProbabilityTheory.Kernel.deterministic_prod_deterministic, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic.{u_1, u_1} (α := α) (mα := mα) (deterministic id ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (mα := mα) (deterministic (fun (x : α) ↦ (x, x)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic.{u_1, u_3} (α := α) (β := PUnit.{u_3 + 1}) (mα := mα) (mβ := PUnit.instMeasurableSpace)
    (deterministic (fun (x : α) ↦ PUnit.unit) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ IsDeterministic (α := α × β) (mα := Prod.instMeasurableSpace) (deterministic Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
mp : IsDeterministic κ → ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
mpr : (∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)) → IsDeterministic κ
⊢ IsDeterministic κ ↔ ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
⊢ IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
⟨fun s hs ↦ ?_⟩

Premises used: MeasureTheory.IsZeroOneMeasure.mk
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
mp :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
refine ⟨fun s hs ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ENNReal)
    ((((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) :
      ENNReal)
    ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) : ENNReal)

Tactic:
have := DFunLike.congr_fun κ.parallelComp_self_comp_copy a |> DFunLike.congr_fun
      <| (s ×ˢ s)
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  Eq (α := ENNReal)
    ((((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) :
      ENNReal)
    ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) : ENNReal)
mp :
  ∀
    (this :
      HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
          ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
        (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
mp₁ mp₂ :
  ∀
    (this :
      HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
          ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
        (((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s)),
    MeasurableSet s
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
rw [parallelComp_comp_copy, prod_apply_prod, copy_comp_apply_prod, inter_self] at this

Premises used: Set.inter_self, ProbabilityTheory.Kernel.copy_comp_apply_prod, ProbabilityTheory.Kernel.parallelComp_comp_copy, ProbabilityTheory.Kernel.prod_apply_prod
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s
pos :
  ∀
    (hκ :
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
        (0 : ENNReal)),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
neg :
  ∀
    (hκ :
      ¬Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
          (0 : ENNReal)),
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
by_cases hκ : κ a s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s
hκ : Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s
hκ : ¬Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ 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 β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s
hκ : ¬Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
exact Or.inr <| (ENNReal.mul_eq_left hκ (by simp)).mp this

Premises used: ENNReal.mul_eq_left, Iff.mp, Or.inr
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s)
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
    (((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s)
⊢ MeasurableSet s

Tactic:
exact hs
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
⊢ IsDeterministic κ

Tactic:
⟨?_⟩

Premises used: ProbabilityTheory.IsDeterministic.mk
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
mpr : κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ
⊢ IsDeterministic κ

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
mpr :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure (β × β)) ((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β))
      ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β))
⊢ κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
mpr :
  Eq.{u_2 + 1} (α := Measure (β × β)) (Measure.prod ((κ : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a))
    ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a)
⊢ Eq.{u_2 + 1} (α := Measure (β × β)) ((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β))
    ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β))

Tactic:
rw [parallelComp_comp_copy, prod_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.parallelComp_comp_copy
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
⊢ Eq.{u_2 + 1} (α := Measure (β × β)) (Measure.prod ((κ : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a))
    ((copy β ∘ₖ κ : (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 β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
mpr :
  ∀ (s t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
    (((copy β ∘ₖ κ : (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.{u_2 + 1} (α := Measure (β × β)) (Measure.prod ((κ : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a))
    ((copy β ∘ₖ κ : (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 β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
mpr :
  (((κ : (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)
⊢ (((copy β ∘ₖ κ : (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 [copy_comp_apply_prod _ _ hs ht]

Premises used: ProbabilityTheory.Kernel.copy_comp_apply_prod
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (((κ : (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:
measure_inter_eq_prod hs ht

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prod
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (((κ : (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:
exact measure_inter_eq_prod hs ht

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_prod
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsDeterministic κ
⊢ ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
(isDeterministic_iff_isZeroOneMeasure κ).mp ‹_›

Premises used: ProbabilityTheory.Kernel.isDeterministic_iff_isZeroOneMeasure, Iff.mp
-- 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 κ
choose :
  ∀ (f : (a : α) → β)
    (hf :
      ∀ (a : α),
        Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (Measure.dirac (f a) : Measure β)),
    ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf
⊢ ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf

Tactic:
choose f hf using fun a ↦ exists_eq_dirac (μ := κ a)

Premises used: MeasureTheory.IsZeroOneMeasure.exists_eq_dirac
-- 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 β)
⊢ ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf

Tactic:
⟨f, ?_, ?_⟩

Premises used: Exists.intro
-- 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_1 : Measurable f
refine_2 : κ = deterministic f ⋯
⊢ ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf

Tactic:
refine ⟨f, ?_, ?_⟩
-- 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
simp_rw : Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s} {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1}
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s}
    {x : α |
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)}

Tactic:
simp_rw [hf, Measure.dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_apply'
-- 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
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | f x ∈ s} x ↔
      Membership.mem (γ := Set α) {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1} x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s} {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1}

Tactic:
ext x
-- 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
x : α
⊢ Membership.mem (γ := Set α) {x : α | f x ∈ s} x ↔
    Membership.mem (γ := Set α) {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1} x

Tactic:
(indicator_eq_one_iff_mem ENNReal).symm

Premises used: Set.Mem, Set.indicator, setOf, ENNReal, Iff.symm, Set.indicator_eq_one_iff_mem
-- 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
x : α
⊢ Membership.mem (γ := Set α) {x : α | f x ∈ s} x ↔
    Membership.mem (γ := Set α) {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1} x

Tactic:
exact (indicator_eq_one_iff_mem ENNReal).symm

Premises used: ENNReal, Iff.symm, Set.indicator_eq_one_iff_mem
-- 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
⊢ f ⁻¹' s =
    preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1}

Tactic:
have : f ⁻¹' s = (fun a => κ a s) ⁻¹' {1} := by
      simp only [preimage, mem_singleton_iff]
      simp_rw [hf, Measure.dirac_apply' _ hs]
      ext x
      exact (indicator_eq_one_iff_mem ENNReal).symm
-- 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}
refine_1 :
  MeasurableSet.{u_1} (α := α)
    (preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1})
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [this]