awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : β × α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((prodMkRight α 0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
h :
  ∀ (a : γ × α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((prodMkLeft γ (κ + η) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((HAdd.hAdd (α := Kernel (γ × α) β) (prodMkLeft γ κ) (prodMkLeft γ η) : (a : γ × α) → Measure β) a :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ prodMkLeft γ (κ + η) = HAdd.hAdd (α := Kernel (γ × α) β) (prodMkLeft γ κ) (prodMkLeft γ η)

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a : γ × α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((prodMkLeft γ (κ + η) : (a : γ × α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((HAdd.hAdd (α := Kernel (γ × α) β) (prodMkLeft γ κ) (prodMkLeft γ η) : (a : γ × α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
h :
  ∀ (a : α × γ) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((prodMkRight γ (κ + η) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((HAdd.hAdd (α := Kernel (α × γ) β) (prodMkRight γ κ) (prodMkRight γ η) : (a : α × γ) → Measure β) a :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ prodMkRight γ (κ + η) = HAdd.hAdd (α := Kernel (α × γ) β) (prodMkRight γ κ) (prodMkRight γ η)

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a : α × γ
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((prodMkRight γ (κ + η) : (a : α × γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((HAdd.hAdd (α := Kernel (α × γ) β) (prodMkRight γ κ) (prodMkRight γ η) : (a : α × γ) → Measure β) a :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
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∞)
⊢ Eq (α := Kernel (γ × α) β) (Kernel.sum fun (i : ι) ↦ prodMkLeft γ (κ i)) (prodMkLeft γ (Kernel.sum κ))

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
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∞)
⊢ 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:
simp_rw [sum_apply, prodMkLeft_apply, sum_apply]

Premises used: ProbabilityTheory.Kernel.prodMkLeft_apply, ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
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∞)
⊢ Eq (α := Kernel (α × γ) β) (Kernel.sum fun (i : ι) ↦ prodMkRight γ (κ i)) (prodMkRight γ (Kernel.sum κ))

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
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∞)
⊢ 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:
simp_rw [sum_apply, prodMkRight_apply, sum_apply]

Premises used: ProbabilityTheory.Kernel.prodMkRight_apply, ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
ca : γ × α
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) ca = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) ca.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
ca : α × γ
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂(prodMkRight γ κ : (a : α × γ) → Measure β) ca = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) ca.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := γ × α) (mα := Prod.instMeasurableSpace) (κ.comap Prod.snd ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := α × γ) (mα := Prod.instMeasurableSpace) (κ.comap Prod.fst ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := γ × α) (mα := Prod.instMeasurableSpace) (κ.comap Prod.snd ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := α × γ) (mα := Prod.instMeasurableSpace) (κ.comap Prod.fst ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := γ × α) (mα := Prod.instMeasurableSpace) (κ.comap Prod.snd ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := α × γ) (mα := Prod.instMeasurableSpace) (κ.comap Prod.fst ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := γ × α) (mα := Prod.instMeasurableSpace) (κ.comap Prod.snd ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α := α × γ) (mα := Prod.instMeasurableSpace) (κ.comap Prod.fst ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
refine : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) → IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ)
⊢ Measurable (β := Unit × α) fun (a : α) ↦ ((), a)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ)
change : IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) (fun (a : α) ↦ ((), a)) ⋯)
⊢ IsSFiniteKernel κ

Tactic:
change IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a ↦ ((), a)) (by fun_prop))

Premises used: Unit.unit, ProbabilityTheory.Kernel.comap, ProbabilityTheory.IsSFiniteKernel, Prod.mk, Unit, ProbabilityTheory.Kernel.prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ)
⊢ IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkLeft Unit κ) (fun (a : α) ↦ ((), a)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
refine : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) → IsSFiniteKernel κ
⊢ IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ)
⊢ Measurable (β := α × Unit) fun (a : α) ↦ (a, ())

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ)
change : IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) (fun (a : α) ↦ (a, ())) ⋯)
⊢ IsSFiniteKernel κ

Tactic:
change IsSFiniteKernel ((prodMkRight Unit κ).comap (fun a ↦ (a, ())) (by fun_prop))

Premises used: Unit.unit, ProbabilityTheory.Kernel.comap, ProbabilityTheory.IsSFiniteKernel, Prod.mk, ProbabilityTheory.Kernel.prodMkRight, Unit
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ)
⊢ IsSFiniteKernel (comap (mα := Prod.instMeasurableSpace) (prodMkRight Unit κ) (fun (a : α) ↦ (a, ())) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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))
neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))
⊢ Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.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 δ
γ : Type u_5
inst : MeasurableSpace γ
κ : Kernel α β
f : β → δ
hf : Measurable f
pos : Eq (α := Kernel (γ × α) δ) (mapOfMeasurable (prodMkLeft γ κ) f ⋯) (prodMkLeft γ (κ.mapOfMeasurable f ⋯))
⊢ Eq (α := Kernel (γ × α) δ) (map (prodMkLeft γ κ) f) (prodMkLeft γ (κ.map f))

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

Premises used: ProbabilityTheory.Kernel.map, reduceDIte
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (γ × α) δ) (mapOfMeasurable (prodMkLeft γ κ) f ⋯) (prodMkLeft γ (κ.mapOfMeasurable f ⋯))

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

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 δ
κ : Kernel α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
pos : ∀ (hf : Measurable f), Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
neg : ∀ (hf : ¬Measurable f), Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))
⊢ Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.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 α β
γ : Type u_5
mγ : MeasurableSpace γ
f : β → δ
hf : Measurable f
pos : Eq (α := Kernel (α × γ) δ) (mapOfMeasurable (prodMkRight γ κ) f ⋯) (prodMkRight γ (κ.mapOfMeasurable f ⋯))
⊢ Eq (α := Kernel (α × γ) δ) (map (prodMkRight γ κ) f) (prodMkRight γ (κ.map f))

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

Premises used: ProbabilityTheory.Kernel.map, reduceDIte
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (α × γ) δ) (mapOfMeasurable (prodMkRight γ κ) f ⋯) (prodMkRight γ (κ.mapOfMeasurable f ⋯))

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

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
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel (β × α) γ) (swapLeft 0) 0

Tactic:
simp [swapLeft]

Premises used: ProbabilityTheory.Kernel.swapLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
⊢ Eq.{u_3 + 1} (α := Measure γ) ((κ.swapLeft : (a : β × α) → Measure γ) a : Measure γ)
    ((κ : (a : α × β) → Measure γ) a.swap : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
s : Set γ
⊢ Eq (α := ℝ≥0∞) ((((κ.swapLeft : (a : β × α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α × β) → Measure γ) a.swap : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
g : γ → ℝ≥0∞
rw rw₁ : ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap = ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap
⊢ ∫⁻ (c : γ), g c ∂(κ.swapLeft : (a : β × α) → Measure γ) a = ∫⁻ (c : γ), g c ∂(κ : (a : α × β) → Measure γ) a.swap

Tactic:
rw [swapLeft_apply]

Premises used: ProbabilityTheory.Kernel.swapLeft_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (κ.comap Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (κ.comap Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 (κ.comap Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_5
x : MeasurableSpace γ
⊢ Eq (α := Kernel (α × γ) β) (swapLeft (prodMkLeft γ κ)) (prodMkRight γ κ)

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.prodMkRight, rfl, ProbabilityTheory.Kernel.prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_5
x : MeasurableSpace γ
⊢ Eq (α := Kernel (γ × α) β) (swapLeft (prodMkRight γ κ)) (prodMkLeft γ κ)

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.prodMkRight, rfl, ProbabilityTheory.Kernel.prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight = κ.map Prod.swap

Tactic:
simp [swapRight]

Premises used: ProbabilityTheory.Kernel.swapRight
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel α (γ × β)) (swapRight 0) 0

Tactic:
simp [swapRight]

Premises used: ProbabilityTheory.Kernel.swapRight
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
⊢ Eq (α := Measure (γ × β)) ((κ.swapRight : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    (Measure.map Prod.swap ((κ : (a : α) → Measure (β × γ)) a) : Measure (γ × β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.swap ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.swap ∈ s} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.swap ∈ s} : ℝ≥0∞)

Tactic:
rw [swapRight_apply, Measure.map_apply measurable_swap hs]

Premises used: ProbabilityTheory.Kernel.swapRight_apply, MeasureTheory.Measure.map_apply, measurable_swap
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.swap ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.swap ∈ s} : ℝ≥0∞)

Tactic:
rfl