awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
b : α
hb : b ∉ s
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)

Tactic:
simpa [hb, piecewise] using hs _ hb

Premises used: ProbabilityTheory.Kernel.piecewise
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
obtain :
  ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
obtain₁ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
    ∃ (η : Kernel α β),
      Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
        IsMarkovKernel η
obtain₂ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
    ∃ (η : Kernel α β),
      Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
        IsMarkovKernel η
refine_1 :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
      (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)
refine_2 refine_2₁ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
    IsMarkovKernel (piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ)
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η

Tactic:
classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using hs _ ha
    · simpa [hb, piecewise] using hs _ hb

Premises used: ProbabilityTheory.Kernel.piecewise
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ (boolKernel μ ν : (a : Bool) → Measure α) false = μ

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ (boolKernel μ ν : (a : Bool) → Measure α) true = ν

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
b : Bool
⊢ (boolKernel μ ν : (a : Bool) → Measure α) b = if b = true then ν else μ

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
b : Bool
false :
  LE.le (α := ℝ≥0∞)
    ((((boolKernel μ ν : (a : Bool) → Measure α) Bool.false : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (max ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ((ν : (a : Set α) → ℝ≥0∞) Set.univ) : ℝ≥0∞)
true :
  LE.le (α := ℝ≥0∞)
    ((((boolKernel μ ν : (a : Bool) → Measure α) Bool.true : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (max ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ((ν : (a : Set α) → ℝ≥0∞) Set.univ) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (max ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ((ν : (a : Set α) → ℝ≥0∞) Set.univ) : ℝ≥0∞)

Tactic:
cases b
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ LE.le (α := ℝ≥0∞)
    ((((boolKernel μ ν : (a : Bool) → Measure α) false : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (max ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ((ν : (a : Set α) → ℝ≥0∞) Set.univ) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ LE.le (α := ℝ≥0∞)
    ((((boolKernel μ ν : (a : Bool) → Measure α) true : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (max ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ((ν : (a : Set α) → ℝ≥0∞) Set.univ) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
b : Bool
false : IsProbabilityMeasure.{u_1} (α := α) (m0 := mα) ((boolKernel μ ν : (a : Bool) → Measure α) Bool.false)
true : IsProbabilityMeasure.{u_1} (α := α) (m0 := mα) ((boolKernel μ ν : (a : Bool) → Measure α) Bool.true)
⊢ IsProbabilityMeasure.{u_1} (α := α) (m0 := mα) ((boolKernel μ ν : (a : Bool) → Measure α) b)

Tactic:
cases b
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
false : IsProbabilityMeasure μ
⊢ IsProbabilityMeasure.{u_1} (α := α) (m0 := mα) ((boolKernel μ ν : (a : Bool) → Measure α) Bool.false)

Tactic:
simp only [boolKernel_apply, Bool.false_eq_true, ↓reduceIte]

Premises used: ProbabilityTheory.Kernel.boolKernel_apply, Bool.false_eq_true, reduceIte
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 true : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure.{u_1} (α := α) (m0 := mα) ((boolKernel μ ν : (a : Bool) → Measure α) Bool.true)

Tactic:
simp only [boolKernel_apply, Bool.false_eq_true, ↓reduceIte]

Premises used: ProbabilityTheory.Kernel.boolKernel_apply, Bool.false_eq_true, reduceIte
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure μ

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
⊢ IsProbabilityMeasure ν

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
⊢ ∃ (κs : ℕ → Kernel Bool α), (∀ (n : ℕ), IsFiniteKernel (κs n)) ∧ boolKernel μ ν = Kernel.sum κs

Tactic:
⟨fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n), fun n ↦ inferInstance, ?_⟩

Premises used: inferInstance, And.intro, Exists.intro, ProbabilityTheory.Kernel.boolKernel, MeasureTheory.sfiniteSeq
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
refine : boolKernel μ ν = Kernel.sum fun (n : ℕ) ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)
⊢ ∃ (κs : ℕ → Kernel Bool α), (∀ (n : ℕ), IsFiniteKernel (κs n)) ∧ boolKernel μ ν = Kernel.sum κs

Tactic:
refine ⟨fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n), fun n ↦ inferInstance, ?_⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
h :
  ∀ (b : Bool) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((((Kernel.sum fun (n : ℕ) ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) b :
                Measure α) :
              (a : Set α) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ boolKernel μ ν = Kernel.sum fun (n : ℕ) ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)

Tactic:
ext b
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
b : Bool
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) b :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) b : Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Kernel.sum_apply]

Premises used: ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
b : Bool
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) false : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) false :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) true : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) true :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) b :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
cases b
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) false : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) false :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [sum_sfiniteSeq]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((boolKernel μ ν : (a : Bool) → Measure α) true : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ (boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n) : (a : Bool) → Measure α) true :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [sum_sfiniteSeq]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
h :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : Bool) → Measure α) false : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((((boolKernel ((κ : (a : Bool) → Measure α) false) ((κ : (a : Bool) → Measure α) true) :
                    (a : Bool) → Measure α)
                  false :
                Measure α) :
              (a : Set α) → ℝ≥0∞)
            s :
          ℝ≥0∞)
h₁ :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : Bool) → Measure α) true : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((((boolKernel ((κ : (a : Bool) → Measure α) false) ((κ : (a : Bool) → Measure α) true) :
                    (a : Bool) → Measure α)
                  true :
                Measure α) :
              (a : Set α) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ κ = boolKernel ((κ : (a : Bool) → Measure α) false) ((κ : (a : Bool) → Measure α) true)

Tactic:
ext (_ | _)
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Bool) → Measure α) false : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((boolKernel ((κ : (a : Bool) → Measure α) false) ((κ : (a : Bool) → Measure α) true) : (a : Bool) → Measure α)
              false :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Bool) → Measure α) true : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((boolKernel ((κ : (a : Bool) → Measure α) false) ((κ : (a : Bool) → Measure α) true) : (a : Bool) → Measure α)
              true :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ : X.Hom Y
⊢ IsSFiniteKernel κ.hom

Tactic:
κ.property

Premises used: SFinKer.Hom.property
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
W X Y Z : SFinKer
κ : W.Hom X
η : X.Hom Y
ξ : Y.Hom Z
⊢ { hom := ξ.hom ∘ₖ { hom := η.hom ∘ₖ κ.hom, property := ⋯ : W.Hom Y }.hom, property := ⋯ : W.Hom Z } =
    { hom := { hom := ξ.hom ∘ₖ η.hom, property := ⋯ : X.Hom Z }.hom ∘ₖ κ.hom, property := ⋯ }

Tactic:
simp [Kernel.comp_assoc]

Premises used: ProbabilityTheory.Kernel.comp_assoc
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
κ η : X ⟶ Y
h : κ.hom = η.hom
⊢ κ = η

Tactic:
SFinKer.Hom.ext h

Premises used: SFinKer.Hom.ext
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ IsSFiniteKernel.{u, u} (α := (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier) (mα :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).str) (Kernel.deterministic Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ IsSFiniteKernel.{u, u} (α := (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X).carrier) (mα :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X).str) (Kernel.deterministic Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
refine_1 :
  CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
      { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }
      { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
refine_2 :
  CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
      { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }
      { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
⊢ MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y ≅
    MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X

Tactic:
refine ⟨⟨Kernel.swap _ _, by rw [Kernel.swap]; infer_instance⟩,
      ⟨Kernel.swap _ _, by rw [Kernel.swap]; infer_instance⟩, ?_, ?_⟩
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
refine_1 :
  Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y))
⊢ CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
      { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }
      { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y))

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
refine_2 :
  Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X))
⊢ CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
      { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }
      { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X)

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y : SFinKer
⊢ Hom.hom
      (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y X))

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
κ : Y ⟶ Z
h :
  Eq (α :=
    Kernel (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X).carrier)
    (Hom.hom
      (X ◁ κ ≫
        Iso.hom
          { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Hom.hom
      (Iso.hom
          { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
        κ ▷ X))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X)
    (X ◁ κ ≫
      Iso.hom
        { hom := { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ })
    (Iso.hom
        { hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
          inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      κ ▷ X)

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
κ : Y ⟶ Z
⊢ Eq (α := Kernel (X.carrier × Y.carrier) (Z.carrier × X.carrier))
    (Kernel.swap X.carrier Z.carrier ∘ₖ (Kernel.id ∥ₖ κ.hom)) (κ.hom ∥ₖ Kernel.id ∘ₖ Kernel.swap X.carrier Y.carrier)

Tactic:
Kernel.swap_parallelComp

Premises used: ProbabilityTheory.Kernel.swap_parallelComp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
κ : Y ⟶ Z
⊢ Eq (α := Kernel (X.carrier × Y.carrier) (Z.carrier × X.carrier))
    (Kernel.swap X.carrier Z.carrier ∘ₖ (Kernel.id ∥ₖ κ.hom)) (κ.hom ∥ₖ Kernel.id ∘ₖ Kernel.swap X.carrier Y.carrier)

Tactic:
exact Kernel.swap_parallelComp

Premises used: ProbabilityTheory.Kernel.swap_parallelComp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X_1 Y : SFinKer
κ : X_1 ⟶ Y
X : SFinKer
h :
  Eq (α :=
    Kernel (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X_1 X).carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier)
    (Hom.hom
      (κ ▷ X ≫
        Iso.hom
          { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Hom.hom
      (Iso.hom
          { hom := { hom := Kernel.swap X_1.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier X_1.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
        X ◁ κ))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X_1 X ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y)
    (κ ▷ X ≫
      Iso.hom
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ })
    (Iso.hom
        { hom := { hom := Kernel.swap X_1.carrier X.carrier, property := ⋯ },
          inv := { hom := Kernel.swap X.carrier X_1.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      X ◁ κ)

Tactic:
ext : 1
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X_1 Y : SFinKer
κ : X_1 ⟶ Y
X : SFinKer
⊢ Eq (α := Kernel (X_1.carrier × X.carrier) (X.carrier × Y.carrier))
    (Kernel.swap Y.carrier X.carrier ∘ₖ (κ.hom ∥ₖ Kernel.id)) (Kernel.id ∥ₖ κ.hom ∘ₖ Kernel.swap X_1.carrier X.carrier)

Tactic:
Kernel.swap_parallelComp

Premises used: ProbabilityTheory.Kernel.swap_parallelComp
-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X_1 Y : SFinKer
κ : X_1 ⟶ Y
X : SFinKer
⊢ Eq (α := Kernel (X_1.carrier × X.carrier) (X.carrier × Y.carrier))
    (Kernel.swap Y.carrier X.carrier ∘ₖ (κ.hom ∥ₖ Kernel.id)) (Kernel.id ∥ₖ κ.hom ∘ₖ Kernel.swap X_1.carrier X.carrier)

Tactic:
exact Kernel.swap_parallelComp

Premises used: ProbabilityTheory.Kernel.swap_parallelComp