import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Probability.Kernel.Composition.Prod
import Mathlib.Probability.Kernel.Composition.CompProd
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Lean.Elab.Tactic.Location
import Lean.Meta.DecLevel
import Lean.Meta.Transform
import Lean.Util.Recognizers
import Lean.Meta.Tactic.Replace
import Lean.Meta.Tactic.Rewrite
import Mathlib.Probability.Kernel.Deterministic
import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.Probability.Kernel.Category.SFinKer
import Mathlib.MeasureTheory.Integral.Lebesgue.Countable

/-! # Standalone extraction for `transformHomToKernel`
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 Lean
end Lean
namespace Lean.Meta
end Lean.Meta
namespace ProbabilityTheory
end ProbabilityTheory
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.Tactic.HomKernel ═══
section
public meta section
open Lean Elab Tactic Meta CategoryTheory Parser.Tactic ProbabilityTheory MonoidalCategory
open ProbabilityTheory.Kernel

/-- Recursive transformation from morphism expression in `SFinKer` to kernel expression. -/
partial def transformHomToKernel (e : Expr) (proofs : List Expr) :
    MetaM (Expr × List Expr) := do
  match e.getAppFn with
  | Expr.const ``tensorHom _ =>
    let args := e.getAppArgs
    let κ := args[args.size - 2]!
    let η := args[args.size - 1]!
    let ST := args[args.size - 3]!
    let SZ := args[args.size - 4]!
    let SY := args[args.size - 5]!
    let SX := args[args.size - 6]!
    let (κ', proofs_κ) ← transformHomToKernel κ proofs
    let (η', proofs_η) ← transformHomToKernel η proofs_κ
    let (X, Y, _, _) ← getTypesFromKernel κ'
    let (Z, T, _, _) ← getTypesFromKernel η'
    let parallelComp_hom_proof ← mkAppMInst ``parallelComp_hom
        #[SX, SY, SZ, ST, ← idME X, ← idME Y, ← idME Z, ← idME T, κ', η'] 2
    return (← mkAppM ``Kernel.parallelComp #[κ', η'], parallelComp_hom_proof :: proofs_η)
  | Expr.const ``CategoryStruct.comp _ =>
    let args := e.getAppArgs
    let κ := args[args.size - 2]!
    let η := args[args.size - 1]!
    let SY := args[args.size - 3]!
    let SX := args[args.size - 4]!
    let SZ := args[args.size - 5]!
    let (κ', proofs_κ) ← transformHomToKernel κ proofs
    let (η', proofs_η) ← transformHomToKernel η proofs_κ
    let (X, Y, _, _) ← getTypesFromKernel η'
    let (Z, _, _, _) ← getTypesFromKernel κ'
    let comp_hom_proof ← mkAppMInst ``comp_hom
        #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, η', κ'] 2
    return (← mkAppM ``Kernel.comp #[η', κ'], comp_hom_proof :: proofs_η)
  | Expr.const ``CategoryStruct.id [xLvl, _] =>
    let args := e.getAppArgs
    let SX := args[args.size - 1]!
    let X ← getTypeFromSFinKer SX
    let mX' ← synthInstance (mkApp (mkConst ``MeasurableSpace [xLvl]) X)
    let id ← mkAppOptM ``Kernel.id #[X, mX']
    let id_hom_proof ← mkAppM ``id_hom #[SX, ← idME X]
    return (id, id_hom_proof :: proofs)
  | Expr.const ``ComonObj.counit [xLvl, _] =>
    let args := e.getAppArgs
    let SX := args[args.size - 2]!
    let X ← getTypeFromSFinKer SX
    let discard_kernel_const := mkConst ``Kernel.discard [xLvl, xLvl]
    let discard_const := mkConst ``counit [xLvl, xLvl, xLvl]
    let discard_hom_proof ← mkAppM' discard_const #[SX, ← idME X]
    return (← mkAppOptM' discard_kernel_const #[X, none], discard_hom_proof :: proofs)
  | Expr.const ``ComonObj.comul [xLvl, _] =>
    let args := e.getAppArgs
    let SX := args[args.size - 2]!
    let X ← getTypeFromSFinKer SX
    let copy_kernel_const := mkConst ``Kernel.copy [xLvl]
    let copy_hom_proof ← mkAppM ``comul #[SX, ← idME X]
    return (← mkAppOptM' copy_kernel_const #[X, none], copy_hom_proof :: proofs)
  | Expr.const ``Kernel.hom _ =>
    let args := e.getAppArgs
    let κ := args[args.size - 2]!
    return (κ, proofs)
  | Expr.const ``MonoidalCategory.whiskerLeft [eLvl, _] =>
    let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl true
    let (κ', proofs_κ) ← transformHomToKernel κ proofs
    let whisker_left_hom_proof ← mkAppMInst ``Kernel.whiskerLeft
      #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1
    return (← mkAppM ``Kernel.parallelComp #[kernel_id, κ'], whisker_left_hom_proof :: proofs_κ)
  | Expr.const ``MonoidalCategory.whiskerRight [eLvl, _] =>
    let (κ, kernel_id, SX, SY, SZ, X, Y, Z) ← deconstructWhiskersHomArgs e eLvl false
    let (κ', proofs_κ) ← transformHomToKernel κ proofs
    let whisker_right_hom_proof ← mkAppMInst ``Kernel.whiskerRight
      #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, κ'] 1
    return (← mkAppM ``Kernel.parallelComp #[κ', kernel_id], whisker_right_hom_proof :: proofs_κ)
  | Expr.const ``Iso.hom _ =>
    let args := e.getAppArgs
    let iso := args[args.size - 1]!
    match iso.getAppFn with
    | Expr.const ``BraidedCategory.braiding _ =>
      let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso
      return (braiding_expr, swap_hom_proof :: proofs)
    | Expr.const ``leftUnitor [eLvl, _] =>
      let (left_unitor_expr, left_unitor_hom_proof) ← deconstructUnitors iso eLvl true true
      return (left_unitor_expr, left_unitor_hom_proof :: proofs)
    | Expr.const ``rightUnitor [eLvl, _] =>
      let (right_unitor_expr, right_unitor_hom_proof) ← deconstructUnitors iso eLvl false true
      return (right_unitor_expr, right_unitor_hom_proof :: proofs)
    | Expr.const ``MonoidalCategory.associator [eLvl, _] =>
      let (associator_expr, associator_hom_proof) ← deconstructAssociator iso eLvl true
      return (associator_expr, associator_hom_proof :: proofs)
    | _ => throwError "Unexpected isomorphism {iso}."
  | Expr.const ``Iso.inv _ =>
    let args := e.getAppArgs
    let iso := args[args.size - 1]!
    match iso.getAppFn with
    | Expr.const ``BraidedCategory.braiding _ =>
      let (braiding_expr, swap_hom_proof) ← deconstructBraiding iso
      return (braiding_expr, swap_hom_proof :: proofs)
    | Expr.const ``leftUnitor [eLvl, _] =>
      let (left_unitor_expr, left_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl true false
      return (left_unitor_expr, left_unitor_inv_hom_proof :: proofs)
    | Expr.const ``rightUnitor [eLvl, _] =>
      let (right_unitor_expr, right_unitor_inv_hom_proof) ← deconstructUnitors iso eLvl false false
      return (right_unitor_expr, right_unitor_inv_hom_proof :: proofs)
    | Expr.const ``MonoidalCategory.associator [eLvl, _] =>
      let (associator_expr, associator_inv_hom_proof) ← deconstructAssociator iso eLvl false
      return (associator_expr, associator_inv_hom_proof :: proofs)
    | _ => throwError "Unexpected isomorphism {iso}."
  | _ => throwError "Expected a hom expression, got: {e}."

end