awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
have this : ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
Tactic: have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hf; exact hf.fst
-- 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 α β
f : β → γ
hf : Measurable f
⊢ fst.{u_1, u_2, u_3} (γ := γ) (mγ := mγ) (κ.map fun (a : β) ↦ (a, f a)) = κ
have rw : (κ.map fun (a : β) ↦ a) = κ
Tactic: rw [fst_map_prod _ hf, Kernel.map_id']
-- 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 α β
f : β → γ
hf : Measurable f
rw : (κ.map fun (a : β) ↦ a) = κ
⊢ fst.{u_1, u_2, u_3} (γ := γ) (mγ := mγ) (κ.map fun (a : β) ↦ (a, f a)) = κ
have rw₁ : κ = κ
Tactic: rw [fst_map_prod _ hf, Kernel.map_id']
-- 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 α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((Measure.map (α := β × γ) Prod.snd ((κ : (a : α) → Measure (β × γ)) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
Tactic: rw [snd_apply, Measure.map_apply measurable_snd hs]
-- 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 α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.map (α := β × γ) Prod.snd ((κ : (a : α) → Measure (β × γ)) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
Tactic: rw [snd_apply, Measure.map_apply measurable_snd hs]
-- 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 α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(κ.snd : (a : α) → Measure γ) a = ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
have rw : ∫⁻ (c : γ), g c ∂((κ.map Prod.snd : Kernel α γ) : (a : α) → Measure γ) a =
  ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [snd_eq, lintegral_map _ measurable_snd a hg]
-- 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 α (β × γ)
a : α
g : γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : γ), g c ∂((κ.map Prod.snd : Kernel α γ) : (a : α) → Measure γ) a =
    ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : γ), g c ∂(κ.snd : (a : α) → Measure γ) a = ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
have rw₁ : ∫⁻ (a : β × γ), g a.2 ∂(κ : (a : α) → Measure (β × γ)) a = ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [snd_eq, lintegral_map _ measurable_snd a hg]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
⊢ IsMarkovKernel κ.snd
have rw : IsMarkovKernel (mβ := mγ) (κ.map Prod.snd)
Tactic: rw [Kernel.snd_eq]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel κ.snd
have rw : IsZeroOrMarkovKernel (mβ := mγ) (κ.map Prod.snd)
Tactic: rw [Kernel.snd_eq]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsFiniteKernel κ
⊢ IsFiniteKernel κ.snd
have rw : IsFiniteKernel (mβ := mγ) (κ.map Prod.snd)
Tactic: rw [Kernel.snd_eq]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsSFiniteKernel κ
⊢ IsSFiniteKernel κ.snd
have rw : IsSFiniteKernel (mβ := mγ) (κ.map Prod.snd)
Tactic: rw [Kernel.snd_eq]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.snd
⊢ IsFiniteKernel κ
have refine : ∀ (a : α),
  LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine ⟨(snd κ).bound, (snd κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (snd κ) a Set.univ)⟩
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.snd
a : α
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' Set.univ) : ℝ≥0∞)
Tactic: rw [snd_apply' _ _ MeasurableSet.univ]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
have pos : ∀ (hg : Measurable g),
  Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
Tactic: by_cases hg : Measurable g
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
pos :
  ∀ (hg : Measurable g),
    Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
have neg : ∀ (hg : ¬Measurable g),
  Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
Tactic: by_cases hg : Measurable g
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
have pos : ∀ (x : α) (s : Set δ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x)) : (a : α) → Measure δ) x : Measure δ) :
          (a : Set δ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((κ.map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s hs
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x)) : (a : α) → Measure δ) x : Measure δ) :
          (a : Set δ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((κ.map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
      (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) (Prod.snd ⁻¹' s)) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
Tactic: rw [snd_apply' _ _ hs, map_apply' _ (hf.prod hg), map_apply' _ hg _ hs]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) (Prod.snd ⁻¹' s)) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x)) : (a : α) → Measure δ) x : Measure δ) :
          (a : Set δ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((κ.map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : MeasurableSet (α := γ × δ) (Prod.snd ⁻¹' s)
Tactic: rw [snd_apply' _ _ hs, map_apply' _ (hf.prod hg), map_apply' _ hg _ hs]
-- 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
⊢ ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
have contrapose : ∀ (hg : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)), Measurable g
Tactic: contrapose hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
have this : ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
Tactic: have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hg; exact hg.snd
-- 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 α β
f : β → γ
hf : Measurable f
⊢ snd.{u_1, u_3, u_2} (β := γ) (mβ := mγ) (κ.map fun (a : β) ↦ (f a, a)) = κ
have rw : (κ.map fun (a : β) ↦ a) = κ
Tactic: rw [snd_map_prod _ hf, Kernel.map_id']
-- 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 α β
f : β → γ
hf : Measurable f
rw : (κ.map fun (a : β) ↦ a) = κ
⊢ snd.{u_1, u_3, u_2} (β := γ) (mβ := mγ) (κ.map fun (a : β) ↦ (f a, a)) = κ
have rw₁ : κ = κ
Tactic: rw [snd_map_prod _ hf, Kernel.map_id']
-- 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 α (β × γ)
⊢ κ.swapRight.fst = κ.snd
have h : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ.swapRight.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- 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 α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
      {p : β × γ | Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ s} p.swap} :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
Tactic: rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]
-- 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 α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ s} p.swap} :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : MeasurableSet (α := γ × β) {p : γ × β | p.1 ∈ s}
Tactic: rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]
-- 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 α (β × γ)
⊢ κ.swapRight.snd = κ.fst
have h : ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ.swapRight.snd : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- 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 α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.snd : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
      {p : β × γ | Membership.mem (γ := Set (γ × β)) (Prod.snd ⁻¹' s) p.swap} :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
Tactic: rw [snd_apply' _ _ hs, swapRight_apply', fst_apply' _ _ hs]
-- 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 α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) (Prod.snd ⁻¹' s) p.swap} :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.snd : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : MeasurableSet (α := γ × β) (Prod.snd ⁻¹' s)
Tactic: rw [snd_apply' _ _ hs, swapRight_apply', fst_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 δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
⊢ IsMarkovKernel κ
have refine : ∀ (x : α × β),
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: refine ⟨fun _ ↦ ⟨?_⟩⟩
-- 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 δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
x : α × β
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ.sectL x.2 : (a : α) → Measure γ) x.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [← sectL_apply, 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 δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
x : α × β
rw :
  Eq (α := ℝ≥0∞) ((((κ.sectL x.2 : (a : α) → Measure γ) x.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← sectL_apply, measure_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 δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
⊢ (κ.sectL b).comap f hf = κ.comap (fun (d : δ) ↦ (f d, b)) ⋯
have h : ∀ (d : δ) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.comap (fun (d : δ) ↦ (f d, b)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext d 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 (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((κ.sectL b : (a : α) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ.comap (fun (d : δ) ↦ (f d, b)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectL_apply, 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 (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectL b : (a : α) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ.comap (fun (d : δ) ↦ (f d, b)) sorry : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectL_apply, 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 (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ.sectL b : (a : α) → Measure γ) (f d) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.sectL b).comap f hf : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.comap (fun (d : δ) ↦ (f d, b)) ⋯ : (a : δ) → Measure γ) d : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α × β) → Measure γ) (f d, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, sectL_apply, comap_apply]
-- 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 δ
κ : Kernel (α × β) γ
inst : ∀ (b : α), IsMarkovKernel (κ.sectR b)
⊢ IsMarkovKernel κ
have refine : ∀ (x : α × β),
  Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: refine ⟨fun _ ↦ ⟨?_⟩⟩