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
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
⊢ Eq (α := Kernel (γ × α) β) (Kernel.sum fun (i : ι) ↦ prodMkLeft γ (κ i)) (prodMkLeft γ (Kernel.sum κ))
have h : ∀ (a : γ × α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ prodMkLeft γ (κ i) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((prodMkLeft γ (Kernel.sum κ) : (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 γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
a : γ × α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ prodMkLeft γ (κ i) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((prodMkLeft γ (Kernel.sum κ) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((Measure.sum fun (n : ι) ↦ (prodMkLeft γ (κ n) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
    ℝ≥0∞)
  ((((prodMkLeft γ (Kernel.sum κ) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply, prodMkLeft_apply, sum_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 γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
a : γ × α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (prodMkLeft γ (κ n) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((prodMkLeft γ (Kernel.sum κ) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ prodMkLeft γ (κ i) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((prodMkLeft γ (Kernel.sum κ) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a.2 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((Kernel.sum κ : (a : α) → Measure β) a.2 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply, prodMkLeft_apply, sum_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 γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
⊢ Eq (α := Kernel (α × γ) β) (Kernel.sum fun (i : ι) ↦ prodMkRight γ (κ i)) (prodMkRight γ (Kernel.sum κ))
have h : ∀ (a : α × γ) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ prodMkRight γ (κ i) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((prodMkRight γ (Kernel.sum κ) : (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 γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
a : α × γ
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ prodMkRight γ (κ i) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((prodMkRight γ (Kernel.sum κ) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((Measure.sum fun (n : ι) ↦ (prodMkRight γ (κ n) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
    ℝ≥0∞)
  ((((prodMkRight γ (Kernel.sum κ) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply, prodMkRight_apply, sum_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 γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
a : α × γ
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (prodMkRight γ (κ n) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((prodMkRight γ (Kernel.sum κ) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ prodMkRight γ (κ i) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((prodMkRight γ (Kernel.sum κ) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((Kernel.sum κ : (a : α) → Measure β) a.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply, prodMkRight_apply, sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ
have refine : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) → IsSFiniteKernel κ
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ)
⊢ IsSFiniteKernel κ
have change : IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) (fun (a : α) ↦ ((), a)) sorry)
Tactic: change IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a ↦ ((), a)) (by fun_prop))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) ↔ IsSFiniteKernel κ
have refine : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) → IsSFiniteKernel κ
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ)
⊢ IsSFiniteKernel κ
have change : IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) (fun (a : α) ↦ (a, ())) sorry)
Tactic: change IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a ↦ (a, ())) (by fun_prop))
-- 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 δ
γ : Type u_5
inst : MeasurableSpace γ
κ : Kernel α β
f : β → δ
⊢ Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
have pos : ∀ (hf : Measurable f), Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
Tactic: by_cases hf : Measurable f
-- 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 δ
γ : Type u_5
inst : MeasurableSpace γ
κ : Kernel α β
f : β → δ
pos : ∀ (hf : Measurable f), Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
⊢ Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
have neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
Tactic: by_cases hf : Measurable f
-- 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 δ
γ : Type u_5
inst : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
⊢ Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
have pos : Eq (α := Kernel (γ × α) δ) (mapOfMeasurable (prodMkLeft γ κ) f sorry) (prodMkLeft γ (κ.mapOfMeasurable f sorry))
Tactic: simp only [map, hf, ↓reduceDIte]
-- 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 δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
⊢ Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
have pos : ∀ (hf : Measurable f), Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
Tactic: by_cases hf : Measurable f
-- 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 δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
pos : ∀ (hf : Measurable f), Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
⊢ Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
have neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
Tactic: by_cases hf : Measurable f
-- 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 δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
⊢ Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
have pos : Eq (α := Kernel (α × γ) δ) (mapOfMeasurable (prodMkRight γ κ) f sorry) (prodMkRight γ (κ.mapOfMeasurable f sorry))
Tactic: simp only [map, hf, ↓reduceDIte]
-- 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∞
⊢ ∫⁻ (c : γ), g c ∂(κ.swapLeft : (a : β × α) → Measure γ) a = ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap
have rw : ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap = ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap
Tactic: rw [swapLeft_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 γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.swap ∈ s} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.swap ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.swap ∈ s} : ℝ≥0∞)
Tactic: rw [swapRight_apply, Measure.map_apply measurable_swap 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 ∂(κ.swapRight : (a : α) → Measure (γ × β)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
have rw : ∫⁻ (c : γ × β), g c ∂(κ.map Prod.swap : (a : α) → Measure (γ × β)) a =
  ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [swapRight_eq, lintegral_map _ measurable_swap 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.swap : (a : α) → Measure (γ × β)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : γ × β), g c ∂(κ.swapRight : (a : α) → Measure (γ × β)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
have rw₁ : ∫⁻ (a : β × γ), g a.swap ∂(κ : (a : α) → Measure (β × γ)) a =
  ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [swapRight_eq, lintegral_map _ measurable_swap 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 κ.swapRight
have rw : IsMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
Tactic: rw [Kernel.swapRight_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 κ.swapRight
have rw : IsZeroOrMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
Tactic: rw [Kernel.swapRight_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 κ.swapRight
have rw : IsFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
Tactic: rw [Kernel.swapRight_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 κ.swapRight
have rw : IsSFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
Tactic: rw [Kernel.swapRight_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 γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
Tactic: rw [fst_apply, Measure.map_apply measurable_fst 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 ∂(κ.fst : (a : α) → Measure β) a = ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
have rw : ∫⁻ (c : β), g c ∂((κ.map Prod.fst : Kernel α β) : (a : α) → Measure β) a =
  ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [fst_eq, lintegral_map _ measurable_fst 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.fst : Kernel α β) : (a : α) → Measure β) a =
    ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : β), g c ∂(κ.fst : (a : α) → Measure β) a = ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
have rw₁ : ∫⁻ (a : β × γ), g a.1 ∂(κ : (a : α) → Measure (β × γ)) a = ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
Tactic: rw [fst_eq, lintegral_map _ measurable_fst 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 κ.fst
have rw : IsMarkovKernel (mβ := mβ) (κ.map Prod.fst)
Tactic: rw [Kernel.fst_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 κ.fst
have rw : IsZeroOrMarkovKernel (mβ := mβ) (κ.map Prod.fst)
Tactic: rw [Kernel.fst_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 κ.fst
have rw : IsFiniteKernel (mβ := mβ) (κ.map Prod.fst)
Tactic: rw [Kernel.fst_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 κ.fst
have rw : IsSFiniteKernel (mβ := mβ) (κ.map Prod.fst)
Tactic: rw [Kernel.fst_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 κ.fst
⊢ IsFiniteKernel κ
have refine : ∀ (a : α),
  LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine ⟨(fst κ).bound, (fst κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (fst κ) 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 κ.fst
a : α
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.fst : (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∞)
      {p : β × γ | Membership.mem (γ := Set β) Set.univ p.1} :
    ℝ≥0∞)
Tactic: rw [fst_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 : β → δ
hg : Measurable g
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
have pos : ∀ (hf : Measurable f),
  Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
Tactic: by_cases hf : Measurable f
-- 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 : β → δ
hg : Measurable g
pos :
  ∀ (hf : Measurable f),
    Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
have neg : ∀ (hf : ¬Measurable f),
  Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
Tactic: by_cases hf : Measurable f
-- 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 : β → δ
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 pos : ∀ (x : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((fst.{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 f : 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 : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((fst.{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 f : 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)) {p : γ × δ | p.1 ∈ s}) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ 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 : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) {p : γ × δ | p.1 ∈ s}) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((fst.{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 f : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : MeasurableSet (α := γ × δ) {p : γ × δ | p.1 ∈ s}
Tactic: rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ 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 : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
have contrapose : ∀ (hf : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)), Measurable f
Tactic: contrapose hf
Cleared hypotheses: hf