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 γ
f : β → γ
a : α
s : Set γ
h : MeasurableSet s
pos :
  ∀ (hf : Measurable f),
    Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (hf : ¬Measurable f),
  Eq (α := ℝ≥0∞) ((((map (mβ := mβ) 0 f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
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 β
κ : Kernel α β
⊢ κ.map id = κ
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((((κ.map id : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a
-- 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 γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
g' : γ → ℝ≥0∞
hg : Measurable g'
⊢ ∫⁻ (b : γ), g' b ∂((κ.map f : Kernel α γ) : (a : α) → Measure γ) a = ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (b : γ), g' b ∂Measure.map f ((κ : (a : α) → Measure β) a) = ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a
Tactic: rw [map_apply _ hf, lintegral_map hg hf]
-- 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 γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
g' : γ → ℝ≥0∞
hg : Measurable g'
rw : ∫⁻ (b : γ), g' b ∂Measure.map f ((κ : (a : α) → Measure β) a) = ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : γ), g' b ∂((κ.map f : Kernel α γ) : (a : α) → Measure γ) a = ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a = ∫⁻ (a : β), g' (f a) ∂(κ : (a : α) → Measure β) a
Tactic: rw [map_apply _ hf, lintegral_map hg hf]
-- 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 α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map (⇑f : (a : β) → γ) = η ↔ κ = η.map (⇑f.symm : (a : γ) → β)
have simp_rw : (∀ (a : α),
    Eq.{u_4 + 1} (α := Measure γ) ((κ.map (⇑f : (a : β) → γ) : (a : α) → Measure γ) a : Measure γ)
      ((η : (a : α) → Measure γ) a : Measure γ)) ↔
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.map (⇑f.symm : (a : γ) → β) : (a : α) → Measure β) a : Measure β)
Tactic: simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]
-- 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 α β
f : β ≃ᵐ γ
η : Kernel α γ
simp_rw :
  (∀ (a : α),
      Eq.{u_4 + 1} (α := Measure γ) ((κ.map (⇑f : (a : β) → γ) : (a : α) → Measure γ) a : Measure γ)
        ((η : (a : α) → Measure γ) a : Measure γ)) ↔
    ∀ (a : α),
      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
        ((η.map (⇑f.symm : (a : γ) → β) : (a : α) → Measure β) a : Measure β)
⊢ κ.map (⇑f : (a : β) → γ) = η ↔ κ = η.map (⇑f.symm : (a : γ) → β)
have simp_rw₁ : (∀ (a : α),
    Eq.{u_4 + 1} (α := Measure γ) (Measure.map.{u_2, u_4} (α := β) (⇑f : (a : β) → γ) ((κ : (a : α) → Measure β) a))
      ((η : (a : α) → Measure γ) a)) ↔
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      ((η.map (⇑f.symm : (a : γ) → β) : (a : α) → Measure β) a : Measure β)
Tactic: simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]
-- 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 α β
f : β ≃ᵐ γ
η : Kernel α γ
simp_rw :
  (∀ (a : α),
      Eq.{u_4 + 1} (α := Measure γ) ((κ.map (⇑f : (a : β) → γ) : (a : α) → Measure γ) a : Measure γ)
        ((η : (a : α) → Measure γ) a : Measure γ)) ↔
    ∀ (a : α),
      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
        ((η.map (⇑f.symm : (a : γ) → β) : (a : α) → Measure β) a : Measure β)
simp_rw₁ :
  (∀ (a : α),
      Eq.{u_4 + 1} (α := Measure γ) (Measure.map.{u_2, u_4} (α := β) (⇑f : (a : β) → γ) ((κ : (a : α) → Measure β) a))
        ((η : (a : α) → Measure γ) a)) ↔
    ∀ (a : α),
      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
        ((η.map (⇑f.symm : (a : γ) → β) : (a : α) → Measure β) a : Measure β)
⊢ κ.map (⇑f : (a : β) → γ) = η ↔ κ = η.map (⇑f.symm : (a : γ) → β)
have simp_rw₂ : (∀ (a : α),
    Eq.{u_4 + 1} (α := Measure γ) (Measure.map.{u_2, u_4} (α := β) (⇑f : (a : β) → γ) ((κ : (a : α) → Measure β) a))
      ((η : (a : α) → Measure γ) a)) ↔
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      (Measure.map.{u_4, u_2} (α := γ) (⇑f.symm : (a : γ) → β) ((η : (a : α) → Measure γ) a) : Measure β)
Tactic: simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]
-- 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 α β
inst : IsSFiniteKernel κ
f : β → γ
⊢ Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.map f)
have pos : ∀ (hf : Measurable f), Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.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 α β
inst : IsSFiniteKernel κ
f : β → γ
pos : ∀ (hf : Measurable f), Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.map f)
⊢ Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.map f)
have neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.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 α β
inst : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.map f)
have pos : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f : (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.MapComap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞)
  (∑' (i : ℕ), (((((κ.seq i).map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
  (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s))
Tactic: rw [Kernel.sum_apply, map_apply' κ hf a hs, Measure.sum_apply _ hs, ← measure_sum_seq κ,
      Measure.sum_apply _ (hf hs)]
-- 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 γ
f : β → γ
κ : Kernel α β
inst : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [map_apply' κ hf a MeasurableSet.univ, Set.preimage_univ, 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
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst : IsMarkovKernel κ
hf : Measurable f
a : α
rw :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [map_apply' κ hf a MeasurableSet.univ, Set.preimage_univ, 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
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst : IsMarkovKernel κ
hf : Measurable f
a : α
rw :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [map_apply' κ hf a MeasurableSet.univ, Set.preimage_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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have pos : ∀ (hf : Measurable f), IsZeroOrMarkovKernel (mβ := mγ) (κ.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
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
pos : ∀ (hf : Measurable f), IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have neg : ∀ (hf : ¬Measurable f), IsZeroOrMarkovKernel (mβ := mγ) (κ.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
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have pos : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (mα := mα) (mβ := mγ) (Kernel.map (mβ := mβ) 0 f)
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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
pos :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (mα := mα) (mβ := mγ) (Kernel.map (mβ := mβ) 0 f)
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have pos₁ : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h
-- 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_1 : β → γ
g : γ → α
f : β → γ
hf : Measurable f
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (mα := mα) (mβ := mγ) (Kernel.map (mβ := mβ) 0 f)
have pos : IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
Tactic: simp only [map_zero]
-- 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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
hf : Measurable f
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have this : IsMarkovKernel (mβ := mγ) (κ.map f)
Tactic: have := IsMarkovKernel.map κ hf
-- 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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
have neg : IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
Tactic: simp only [map_of_not_measurable _ hf]
-- 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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
f : β → γ
⊢ IsFiniteKernel (mβ := mγ) (κ.map f)
have refine : ∀ (a : α), ((((κ.map f : Kernel α γ) : (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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
f : β → γ
a : α
⊢ ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
have pos : ∀ (hf : Measurable f),
  ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: by_cases hf : Measurable f
-- 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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
f : β → γ
a : α
pos :
  ∀ (hf : Measurable f),
    ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
have neg : ∀ (hf : ¬Measurable f),
  ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: by_cases hf : Measurable f
-- 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_1 : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
have pos : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) ≤ κ.bound
Tactic: rw [map_apply' κ hf a MeasurableSet.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
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
⊢ Eq (α := Kernel γ β) (map (const γ μ) f) (const γ (Measure.map f μ))
have h : ∀ (x : γ) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.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
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((((const γ μ : Kernel γ α) : (a : γ) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]
-- 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 γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((((const γ μ : Kernel γ α) : (a : γ) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]
-- 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 γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((((const γ μ : Kernel γ α) : (a : γ) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]
-- 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 γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((((const γ μ : Kernel γ α) : (a : γ) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]
-- 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 : γ → α
hg : Measurable g
⊢ Eq (α := Kernel γ β) (comap 0 g hg) 0
have h : ∀ (a : γ) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((comap 0 g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel γ β) : (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 β
κ : Kernel α β
⊢ κ.comap id ⋯ = κ
have h : ∀ (a : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((κ.comap id sorry : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (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
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
⊢ (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comap g hg) = κ.comap g hg
have h : ∀ (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∞)
Tactic: ext a s hs