awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ κ.mapOfMeasurable f hf = κ.map f

Tactic:
simp [map, hf]

Premises used: ProbabilityTheory.Kernel.map
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
⊢ Eq.{u_4 + 1} (α := Measure γ) (((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ)
    (Measure.map f ((κ : (a : α) → Measure β) a) : Measure γ)

Tactic:
simp only [map, hf, ↓reduceDIte, mapOfMeasurable, coe_mk]

Premises used: ProbabilityTheory.Kernel.map, reduceDIte, ProbabilityTheory.Kernel.coe_mk, ProbabilityTheory.Kernel.mapOfMeasurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((Measure.map f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [map_apply _ hf, Measure.map_apply hf hs]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.Measure.map_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
h :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
      (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
⊢ Eq (α := Kernel α δ) (κ.map (g ∘ f)) (map (mβ := mγ) (κ.map f) g)

Tactic:
ext1 x
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
hf : Measurable f
g : γ → δ
hg : Measurable g
x : α
h :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) : Measure δ)
h₁ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map g (Measure.map f ((κ : (a : α) → Measure β) x)) : Measure δ)
h₂ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (Measure.map (g ∘ f) ((κ : (a : α) → Measure β) x) : Measure δ)
h₃ h₄ :
  Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
⊢ Eq.{u_5 + 1} (α := Measure δ) (((κ.map (g ∘ f) : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)
    (((map (mβ := mγ) (κ.map f) g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ)

Tactic:
rw [map_apply _ hg, map_apply _ hf, Measure.map_map hg hf, ← map_apply _ (hg.comp hf)]

Premises used: ProbabilityTheory.Kernel.map_apply, Measurable.comp, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
h :
  ∀ (a : α) (s : Set γ),
    MeasurableSet s →
      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 (α := Kernel α γ) (map (mβ := mβ) 0 f) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
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∞)
⊢ 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

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a : α
s : Set γ
h : MeasurableSet s
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:
simp [map_apply, hf]

Premises used: ProbabilityTheory.Kernel.map_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a : α
s : Set γ
h : MeasurableSet s
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:
simp [map_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
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∞)
⊢ κ.map id = κ

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
h : 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:
simp [map_apply, measurable_id]

Premises used: ProbabilityTheory.Kernel.map_apply, measurable_id
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ (κ.map fun (a : β) ↦ a) = κ

Tactic:
map_id κ

Premises used: ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
rw₁ rw₂ : ∫⁻ (a : β), g' (f a) ∂(κ : (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

Tactic:
rw [map_apply _ hf, lintegral_map hg hf]

Premises used: ProbabilityTheory.Kernel.map_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 β)
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 β)
⊢ κ.map (⇑f : (a : β) → γ) = η ↔ κ = η.map (⇑f.symm : (a : γ) → β)

Tactic:
simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasurableEquiv.symm, MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, ProbabilityTheory.Kernel.ext_iff, MeasurableEquiv.measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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)
neg : ∀ (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)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
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∞)
⊢ Eq (α := Kernel α γ) (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).map f) (κ.map f)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
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))
⊢ 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:
rw [Kernel.sum_apply, map_apply' κ hf a hs, Measure.sum_apply _ hs, ← measure_sum_seq κ,
      Measure.sum_apply _ (hf hs)]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply, ProbabilityTheory.Kernel.measure_sum_seq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
    (∑' (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:
simp_rw [map_apply' _ hf _ hs]

Premises used: ProbabilityTheory.Kernel.map_apply'
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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)

Tactic:
simp [map_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) (((((κ.map f : Kernel α γ) : (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]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasureTheory.IsProbabilityMeasure.measure_univ, Set.preimage_univ, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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)
neg : ∀ (hf : ¬Measurable f), IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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)
pos₁ : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
pos : IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (mα := mα) (mβ := mγ) (Kernel.map (mβ := mβ) 0 f)

Tactic:
simp only [map_zero]

Premises used: ProbabilityTheory.Kernel.map_zero
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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γ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 κ
⊢ IsMarkovKernel (mβ := mγ) (κ.map f)

Tactic:
have := IsMarkovKernel.map κ hf
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 κ
this : IsMarkovKernel (mβ := mγ) (κ.map f)
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
neg : IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel (mβ := mγ) (κ.map f)

Tactic:
simp only [map_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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)

Tactic:
⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩

Premises used: ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, Exists.intro, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 : β → γ
refine :
  ∀ (a : α), ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ IsFiniteKernel (mβ := mγ) (κ.map f)

Tactic:
refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
neg :
  ∀ (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

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
pos : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) ≤ κ.bound
⊢ ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
rw [map_apply' κ hf a MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) ≤ κ.bound

Tactic:
measure_le_bound κ a _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' Set.univ) ≤ κ.bound

Tactic:
exact measure_le_bound κ a _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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

Tactic:
simp [map_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 : IsSFiniteKernel κ
f : β → γ
⊢ IsSFiniteKernel (mβ := mγ) (κ.map f)

Tactic:
⟨⟨fun n => Kernel.map (seq κ n) f, inferInstance, (sum_map_seq κ f).symm⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, ProbabilityTheory.Kernel.map, inferInstance, ProbabilityTheory.Kernel.seq, And.intro, Exists.intro, ProbabilityTheory.Kernel.sum_map_seq, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
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∞)
⊢ Eq (α := Kernel γ β) (map (const γ μ) f) (const γ (Measure.map f μ))

Tactic:
ext x s hs