import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Kernel.Composition.CompProd
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.Probability.Kernel.Deterministic

/-! # Standalone extraction for `ProbabilityTheory.Kernel.comp_lift`
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.EqLift.Kernel.Lift ═══
section
open MeasureTheory ProbabilityTheory MeasurableEquiv
namespace ProbabilityTheory.Kernel
universe x y z w t
variable {X : Type x} [MeasurableSpace X] {Y : Type y} [MeasurableSpace Y] {X' : Type w} [MeasurableSpace X'] {Y' : Type w} [MeasurableSpace Y']

/-- Cast a kernel to different types in the same universe level, using measurable equivalences. -/
noncomputable def lift {ex : X' ≃ᵐ X} {ey : Y' ≃ᵐ Y} (κ : Kernel X Y) : Kernel X' Y' :=
  (κ.map ey.symm).comap ex ex.measurable

variable (ex : X' ≃ᵐ X) (ey : Y' ≃ᵐ Y)
variable {Z : Type z} [MeasurableSpace Z] {T : Type t} [MeasurableSpace T] {Z' : Type w} [MeasurableSpace Z'] {T' : Type w} [MeasurableSpace T'] (ez : Z' ≃ᵐ Z) (et : T' ≃ᵐ T)

lemma comp_lift (η : Kernel X Y) (κ : Kernel Z X) :
    η.lift (ex := ex) (ey := ey) ∘ₖ κ.lift (ex := ez) (ey := ex) =
      (η ∘ₖ κ).lift (ex := ez) (ey := ey) := sorry

end ProbabilityTheory.Kernel
end