awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have h₁ : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
Tactic: rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
Tactic: have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η :=
    MutuallySingular.compProd_of_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
inst_2 : MeasurableSpace.CountableOrCountablyGenerated α β
inst_3 : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) ≪ ν ⊗ₘ η ∧ μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
this : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ.singularPart η : (a : α) → Measure β) a : Measure β) (0 : Measure β)
have refine : μ ⊗ₘ κ.singularPart η = 0
Tactic: refine compProd_eq_zero_iff.mp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
⊢ deterministic f hf ∘ₖ κ = κ.map f
have h : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (b : β),
    (((deterministic f hf : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
Tactic: simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₁ :
  ∫⁻ (b : β),
      (((deterministic f hf : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∫⁻ (b : β), s.indicator (fun (x : γ) ↦ 1) (f b) ∂(κ : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
Tactic: simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₁ :
  ∫⁻ (b : β),
      (((deterministic f hf : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
h₂ :
  ∫⁻ (b : β), s.indicator (fun (x : γ) ↦ 1) (f b) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((deterministic f hf ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s)
Tactic: simp_rw [map_apply' _ hf _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
    lintegral_indicator_const_comp hf hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
⊢ κ ∘ₖ deterministic g hg = κ.comap g hg
have h : ∀ (a : γ) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic 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∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic 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₁ : ∫⁻ (b : α),
    (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s ∂(deterministic g hg : (a : γ) → Measure α) a =
  (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∫⁻ (b : α),
      (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s ∂(deterministic g hg : (a : γ) → Measure α) a =
    (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ ∘ₖ deterministic 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₂ : ∫⁻ (b : α), (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s ∂Measure.dirac (g a) =
  (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
⊢ deterministic g hg ∘ₖ deterministic f hf = deterministic (g ∘ f) ⋯
have h : ∀ (a : β) (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((deterministic g hg ∘ₖ deterministic f hf : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((((deterministic (g ∘ f) sorry : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := Kernel (β × α) (β × α)) (swap α β ∘ₖ swap β α) Kernel.id
have simp_rw : Eq (α := Kernel (β × α) (β × α)) (deterministic Prod.swap sorry ∘ₖ deterministic Prod.swap sorry) Kernel.id
Tactic: simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
simp_rw : Eq (α := Kernel (β × α) (β × α)) (deterministic Prod.swap ⋯ ∘ₖ deterministic Prod.swap ⋯) Kernel.id
⊢ Eq (α := Kernel (β × α) (β × α)) (swap α β ∘ₖ swap β α) Kernel.id
have simp_rw₁ : Eq (α := Kernel (β × α) (β × α)) (deterministic (Prod.swap ∘ Prod.swap) sorry) Kernel.id
Tactic: simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
simp_rw : Eq (α := Kernel (β × α) (β × α)) (deterministic Prod.swap ⋯ ∘ₖ deterministic Prod.swap ⋯) Kernel.id
simp_rw₁ : Eq (α := Kernel (β × α) (β × α)) (deterministic (Prod.swap ∘ Prod.swap) ⋯) Kernel.id
⊢ Eq (α := Kernel (β × α) (β × α)) (swap α β ∘ₖ swap β α) Kernel.id
have simp_rw₂ : Eq (α := Kernel (β × α) (β × α)) (deterministic id sorry) Kernel.id
Tactic: simp_rw [swap, Kernel.deterministic_comp_deterministic, Prod.swap_swap_eq, Kernel.id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ swap β γ ∘ₖ κ = κ.map Prod.swap
have rw : deterministic Prod.swap sorry ∘ₖ κ = κ.map Prod.swap
Tactic: rw [swap, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
rw : deterministic Prod.swap ⋯ ∘ₖ κ = κ.map Prod.swap
⊢ swap β γ ∘ₖ κ = κ.map Prod.swap
have rw₁ : Eq (α := Kernel α (γ × β)) (κ.map Prod.swap) (κ.map Prod.swap)
Tactic: rw [swap, deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
have pos : ∀ (hf : Measurable f), Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
pos : ∀ (hf : Measurable f), Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
have neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
⊢ Eq (α := Kernel α δ) ((η ∘ₖ κ).map f) (η.map f ∘ₖ κ)
have pos : ∀ (a : α) (s : Set δ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((((η ∘ₖ κ).map f : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((η.map f ∘ₖ κ : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((((η ∘ₖ κ).map f : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((η.map f ∘ₖ κ : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (f ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    ((((η.map f : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a
Tactic: rw [map_apply' _ hf _ hs, comp_apply', comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β γ
f : γ → δ
hf : Measurable f
a : α
s : Set δ
hs : MeasurableSet s
pos :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (f ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ((((η.map f : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞) ((((((η ∘ₖ κ).map f : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((η.map f ∘ₖ κ : Kernel α δ) : (a : α) → Measure δ) a : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : MeasurableSet (f ⁻¹' s)
Tactic: rw [map_apply' _ hf _ hs, comp_apply', comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
⊢ η ∘ₖ κ.map f = η.comap f hf ∘ₖ κ
have h : ∀ (x : α) (s : Set δ) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((η ∘ₖ κ.map f : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η.comap f hf ∘ₖ κ : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s ms
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ κ.map f : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η.comap f hf ∘ₖ κ : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : β), (((η : (a : γ) → Measure δ) (f a) : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (b : β), (((η.comap f hf : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x
Tactic: rw [comp_apply' _ _ _ ms, lintegral_map _ hf _ (η.measurable_coe ms), comp_apply' _ _ _ ms]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompMap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ
have simp_rw : Eq (α := Kernel α δ) ((η ∘ₖ κ).map Prod.snd) (η.map Prod.snd ∘ₖ κ)
Tactic: simp_rw [snd_eq, map_comp κ η _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompNotation (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (⇑Kernel.id : (a : α) → Measure α) ∘ₘ μ = μ
have rw : (⇑(Kernel.deterministic id sorry) : (a : α) → Measure α) ∘ₘ μ = μ
Tactic: rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompNotation (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
rw : (⇑(Kernel.deterministic id ⋯) : (a : α) → Measure α) ∘ₘ μ = μ
⊢ (⇑Kernel.id : (a : α) → Measure α) ∘ₘ μ = μ
have rw₁ : map id μ = μ
Tactic: rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompNotation (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
rw : (⇑(Kernel.deterministic id ⋯) : (a : α) → Measure α) ∘ₘ μ = μ
rw₁ : map id μ = μ
⊢ (⇑Kernel.id : (a : α) → Measure α) ∘ₘ μ = μ
have rw₂ : μ = μ
Tactic: rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ @HasFiniteIntegral _ ℝ _ mβ
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
have simp_rw : ∫⁻ (a_1 : β),
    ENNReal.ofReal
      (ENNReal.toReal
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s))) ∂(κ : (a : α) → Measure β) a <
  ∞
Tactic: simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∫⁻ (b : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' s))) ∂(κ : (a : α) → Measure β) a ≤
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
have refine : ∀ᵐ (a_1 : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  ENNReal.ofReal
      (ENNReal.toReal
        ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s))) ≤
    (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t)
Tactic: refine lintegral_mono_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.IntegralCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∀ᵐ (a_1 : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s))) ≤
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t)
have h : ∀ (b : β)
  (hb :
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ENNReal.ofReal
      (ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))) ≤
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
Tactic: filter_upwards [ae_kernel_lt_top a h2s] with b hb