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

/-! # Standalone extraction for `ProbabilityTheory.Kernel.hom_apply`
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 MeasureTheory
end MeasureTheory
namespace ProbabilityTheory
end ProbabilityTheory
namespace MeasurableEquiv
end MeasurableEquiv
namespace ProbabilityTheory.Kernel
end ProbabilityTheory.Kernel

-- ═══ ForMathlib.MeasureTheory.Order.Lattice ═══
section
open Finset
variable {α δ : Type*} [MeasurableSpace δ] [SemilatticeInf α] {m : MeasurableSpace α} [MeasurableInf₂ α]
attribute [to_dual existing] MeasurableInf₂
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 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

lemma hom_apply (κ : Kernel X Y) [IsSFiniteKernel κ] (a : SX) :
    (κ.hom (ex := ex) (ey := ey)).1 a = (κ.map ey.symm) (ex a) := sorry

end
end ProbabilityTheory.Kernel
end