import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Kernel.Deterministic
import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.Probability.Kernel.Category.SFinKer
import Mathlib.Probability.Kernel.Composition.CompProd
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

/-! # Standalone extraction for `ProbabilityTheory.Kernel.monoComp₀`
Definitions are copied verbatim; theorem proofs are replaced by `sorry`.
Auto-generated by Referee. -/

set_option quotPrecheck false

-- Namespace stubs (so later `open`s resolve).
namespace Finset
end Finset
namespace ProbabilityTheory
end ProbabilityTheory
namespace MeasureTheory
end MeasureTheory
namespace ENNReal
end ENNReal
namespace ProbabilityTheory.Kernel
end ProbabilityTheory.Kernel
namespace MeasurableEquiv
end MeasurableEquiv
namespace MeasurableCoherence
end MeasurableCoherence

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
end

-- ═══ Tactic.EqLift.ForMathlib.Kernel ═══
section
open ProbabilityTheory MeasureTheory ENNReal Set
variable {α β γ ι : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace ι]
namespace ProbabilityTheory.Kernel

instance (κ : Kernel α β) [IsDeterministic κ] : IsSFiniteKernel κ := by
  by_contra
  have : ∀ C < ∞, ∃ a, C < (κ a) univ := by
    by_contra! h
    have : IsFiniteKernel κ := ⟨h⟩
    have : IsSFiniteKernel κ := inferInstance
    contradiction
  obtain ⟨a, ha⟩ := this 0 (by simp)
  have h := DFunLike.congr_fun κ.parallelComp_self_comp_copy a
  simp_all only [not_false_eq_true, parallelComp_of_not_isSFiniteKernel_left, zero_comp, zero_apply]
  replace h := DFunLike.congr_fun h Set.univ
  rw [comp_apply'] at h
  · simp_rw [copy_apply, Measure.dirac_apply' _ MeasurableSet.univ, indicator_univ] at h
    simp only [Measure.coe_zero, Pi.zero_apply, Pi.one_apply, MeasureTheory.lintegral_const,
      one_mul] at h
    exact ha.ne h
  exact MeasurableSet.univ

end ProbabilityTheory.Kernel
end

-- ═══ Tactic.KernelHom.Kernel.Hom ═══
section
open MeasureTheory ProbabilityTheory MeasurableEquiv CategoryTheory
open scoped SFinKer CategoryTheory CategoryTheory.MonoidalCategory
namespace ProbabilityTheory.Kernel
variable {X Y T Z : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace T] [MeasurableSpace Z]
section
variable {SX SY ST SZ : SFinKer} {ex : SX ≃ᵐ X} {ey : SY ≃ᵐ Y}

/-- Transform a morphism in `SFinKer` into a kernel. -/
noncomputable def fromHom (κ : SX ⟶ SY) : Kernel X Y := (κ.1.comap ex.symm (sorry)).map ey

/-- Transform a kernel into a morphism in `SFinKer`. -/
noncomputable def hom (κ : Kernel X Y) [IsSFiniteKernel κ] : SX ⟶ SY := by
  refine ⟨(κ.map ey.symm).comap ex (by fun_prop), ?_⟩
  have := κ.2
  infer_instance

end
end ProbabilityTheory.Kernel
end

-- ═══ Tactic.KernelHom.Kernel.MonoidalComp ═══
section
open CategoryTheory MeasureTheory ProbabilityTheory MeasurableEquiv
open scoped MonoidalCategory SFinKer

/-- A class witnessing the existence of a measurable equivalence between two measurable spaces. -/
class MeasurableCoherence (X Y : Type*) [MeasurableSpace X] [MeasurableSpace Y] where
  /-- A measurable equivalence between `X` and `Y`. -/
  miso : X ≃ᵐ Y

namespace MeasurableCoherence
variable {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] [mXY : MeasurableCoherence X Y]

/-- `MeasurableCoherence` gives an instance of `MonoidalCoherence` in the `SFinKer` category. -/
@[reducible]
noncomputable def monoidalCoherence {SX SY : SFinKer} (ex : SX.carrier ≃ᵐ X)
    (ey : SY.carrier ≃ᵐ Y) : MonoidalCoherence SX SY where
  iso := by
    let e := ex.trans <| mXY.miso.trans ey.symm
    refine ⟨⟨Kernel.id.map e, inferInstance⟩,
      ⟨Kernel.id.map e.symm, inferInstance⟩, ?_, ?_⟩
    all_goals ext; dsimp
    · rw [Kernel.id_map (by fun_prop), Kernel.id_map (by fun_prop),
        Kernel.deterministic_comp_deterministic, Kernel.id]
      congr
      simp
    · rw [Kernel.id_map (by fun_prop), Kernel.id_map (by fun_prop),
        Kernel.deterministic_comp_deterministic, Kernel.id]
      congr
      simp

end MeasurableCoherence
namespace ProbabilityTheory.Kernel
open MeasurableCoherence
variable {W X Y Z : Type*} [MeasurableSpace W] [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {SW SX SY SZ : SFinKer} (ew : SW ≃ᵐ W) (ex : SX ≃ᵐ X) (ey : SY ≃ᵐ Y) (ez : SZ ≃ᵐ Z) [MeasurableCoherence X Y] (κ : Kernel W X) [IsSFiniteKernel κ] (η : Kernel Y Z) [IsSFiniteKernel η]

/-- The kernelized version of the monoidal composition of kernels using the `SFinKer` category.
It uses arbitrary measurable equivalences to transport the kernels to the `SFinKer` category. -/
noncomputable def monoComp₀ : Kernel W Z :=
  have := monoidalCoherence ex ey
  fromHom (ex := ew) (ey := ez) <| hom (ex := ew) (ey := ex) κ ⊗≫
    hom (ex := ey) (ey := ez) η

end ProbabilityTheory.Kernel
end