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 β
κ : 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)
⊢ 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)
have 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
Tactic: rw [parallelComp_comp_copy, prod_apply_prod, copy_comp_apply_prod, inter_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hκ : κ a s = 0
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hκ : κ a s = 0
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 κ
have mpr : κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
⊢ κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ
have mpr : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure (β × β)) ((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β))
    ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 (β × β)) ((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β))
    ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β))
have mpr : Eq.{u_2 + 1} (α := Measure (β × β)) (Measure.prod ((κ : (a : α) → Measure β) a) ((κ : (a : α) → Measure β) a))
  ((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a)
Tactic: rw [parallelComp_comp_copy, prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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)
have 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)
Tactic: refine Measure.prod_eq fun s t hs ht ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ (((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)
have 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)
Tactic: rw [copy_comp_apply_prod _ _ hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : StandardBorelSpace β
κ : Kernel α β
inst_1 : IsMarkovKernel κ
inst_2 : IsDeterministic κ
⊢ ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf
have 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
Tactic: choose f hf using fun a ↦ exists_eq_dirac (μ := κ a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
have refine_1 : Measurable f
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ ∃ (f : α → β) (hf : Measurable f), κ = deterministic f hf
have refine_2 : κ = deterministic f sorry
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s}
    {x : α |
      Eq (α := ENNReal) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)}
have simp_rw : Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s} {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1}
Tactic: simp_rw [hf, Measure.dirac_apply' _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ∈ s} {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | f x ∈ s} x ↔
    Membership.mem (γ := Set α) {x : α | Eq (α := ENNReal) (s.indicator 1 (f x)) 1} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (hypothesis)
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
⊢ MeasurableSet (f ⁻¹' s)
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 (f ⁻¹' s)
have refine_1 : MeasurableSet.{u_1} (α := α)
  (preimage (β := ENNReal) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s) {1})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
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 β)
⊢ κ = deterministic f ⋯
have refine_2 : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (((deterministic f sorry : Kernel α β) : (a : α) → Measure β) a : Measure β)
Tactic: ext a : 1
-- 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 (η ∘ₖ κ)
⊢ η ∘ₖ κ ×ₖ κ = η ×ₖ Kernel.id ∘ₖ κ
have h : ∀ (a : α),
  Eq (α := Measure (γ × β)) ((η ∘ₖ κ ×ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
Tactic: ext a : 1
-- 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 : α
⊢ Eq (α := Measure (γ × β)) ((η ∘ₖ κ ×ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
have h : Eq (α := Measure (γ × β)) (Measure.prod ((η ∘ₖ κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure β) a))
  ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a)
Tactic: rw [prod_apply]
-- 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 : α
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((η ∘ₖ κ : (a : α) → Measure γ) a) ((κ : (a : α) → Measure β) a))
    ((η ×ₖ Kernel.id ∘ₖ κ : (a : α) → Measure (γ × β)) a)
have 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)
Tactic: refine Measure.prod_eq fun s t hs ht ↦ ?_
-- 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
⊢ (((η ×ₖ 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)
have 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)
Tactic: rw [comp_apply' _ _ _ (hs.prod ht)]
-- 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
⊢ ∫⁻ (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)
have 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)
Tactic: simp_rw [prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ ht]
-- 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
b : β
⊢ 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
have 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
Tactic: split_ifs
-- 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
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
⊢ 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
have neg : b ∉ t →
  HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (0 : ENNReal) =
    0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (hypothesis)
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) ∂(κ : (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)
have 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
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
-- 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
⊢ ∫⁻ (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)
have 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)
Tactic: simp_rw [this]
-- 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
⊢ ∫⁻ (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)
have 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)
Tactic: rw [lintegral_indicator ht]