awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ((((κ.seq i).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
  (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
Tactic: rw [Kernel.sum_apply, comap_apply' κ hg a s, Measure.sum_apply _ hs, ← measure_sum_seq κ,
    Measure.sum_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsMarkovKernel κ
hg : Measurable g
a : γ
⊢ Eq (α := ℝ≥0∞) ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [comap_apply' κ hg a Set.univ, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsMarkovKernel κ
hg : Measurable g
a : γ
rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [comap_apply' κ hg a Set.univ, measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
have inl : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrMarkovKernel.{u_4, u_2} (β := β) (mβ := mβ) (Kernel.comap 0 g hg)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h
Cleared hypotheses: κ, inst
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel.{u_4, u_2} (β := β) (mβ := mβ) (Kernel.comap 0 g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
have inr : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (κ.comap g hg)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
have this : IsMarkovKernel (κ.comap g hg)
Tactic: have := IsMarkovKernel.comap κ hg
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
⊢ IsFiniteKernel (κ.comap g hg)
have refine : ∀ (a : γ), (((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ (((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
have rw : (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: rw [comap_apply' κ hg a Set.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
⊢ κ.comap (g ∘ f) ⋯ = (κ.comap g hg).comap f hf
have h : ∀ (a : δ) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.comap (g ∘ f) sorry : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((κ.comap g hg).comap f hf : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Kernel α δ) (comap (κ.map g) f hf) ((κ.comap f hf).map g)
have h : ∀ (x : α) (s : Set δ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((((κ.map g : Kernel β δ) : (a : β) → Measure δ) (f x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((((κ.map g : Kernel β δ) : (a : β) → Measure δ) (f x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((((κ.map g : Kernel β δ) : (a : β) → Measure δ) (f x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.map g ((κ.comap f hf : (a : α) → Measure γ) x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((((κ.map g : Kernel β δ) : (a : β) → Measure δ) (f x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g ((κ.comap f hf : (a : α) → Measure γ) x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ map Kernel.id f = deterministic f hf
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((Measure.map f (Measure.dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) (((Measure.map f (Measure.dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ comap Kernel.id f hf = deterministic f hf
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯
have rw : map (mβ := mβ) (map Kernel.id f) g = deterministic (g ∘ f) sorry
Tactic: rw [← id_map, ← map_comp_right _ hf hg, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
rw : map (mβ := mβ) (map Kernel.id f) g = deterministic (g ∘ f) ⋯
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯
have rw₁ : map Kernel.id (g ∘ f) = deterministic (g ∘ f) sorry
Tactic: rw [← id_map, ← map_comp_right _ hf hg, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
rw : map (mβ := mβ) (map Kernel.id f) g = deterministic (g ∘ f) ⋯
rw₁ : map Kernel.id (g ∘ f) = deterministic (g ∘ f) ⋯
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯
have rw₂ : deterministic (g ∘ f) sorry = deterministic (g ∘ f) sorry
Tactic: rw [← id_map, ← map_comp_right _ hf hg, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
rw : map (mβ := mβ) (map Kernel.id f) g = deterministic (g ∘ f) ⋯
rw₁ : map Kernel.id (g ∘ f) = deterministic (g ∘ f) ⋯
rw₂ : deterministic (g ∘ f) ⋯ = deterministic (g ∘ f) ⋯
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯
have rw₃ : Measurable (g ∘ f)
Tactic: rw [← id_map, ← map_comp_right _ hf hg, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel (α × β) γ) (prodMkLeft α 0) 0
have h : ∀ (x : α × β) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((prodMkLeft α 0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel (β × α) γ) (prodMkRight α 0) 0
have h : ∀ (x : β × α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((prodMkRight α 0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
⊢ prodMkLeft γ (κ + η) = HAdd.hAdd (α := Kernel (γ × α) β) (prodMkLeft γ κ) (prodMkLeft γ η)
have h : ∀ (a : γ × α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((prodMkLeft γ (κ + η) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((HAdd.hAdd (α := Kernel (γ × α) β) (prodMkLeft γ κ) (prodMkLeft γ η) : (a : γ × α) → Measure β) a :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
⊢ prodMkRight γ (κ + η) = HAdd.hAdd (α := Kernel (α × γ) β) (prodMkRight γ κ) (prodMkRight γ η)
have h : ∀ (a : α × γ) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((prodMkRight γ (κ + η) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((HAdd.hAdd (α := Kernel (α × γ) β) (prodMkRight γ κ) (prodMkRight γ η) : (a : α × γ) → Measure β) a :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext