import Mathlib.MeasureTheory.Order.Lattice
import Mathlib.Tactic.CategoryTheory.Reassoc
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 `kernelreassocExpr`
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 Mathlib.Tactic
end Mathlib.Tactic

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

-- ═══ Tactic.KernelHom.Tactic.Reassoc ═══
section
public meta section
open Lean Meta Elab Tactic ProbabilityTheory Mathlib.Tactic Reassoc

/-- Reassociates the kernels in the type of `pf` using the registered handlers,
using `kernelReassocHandler` as the default.

Returns the proof of the lemma along with a list of fresh level metavariables. -/
def kernelreassocExpr (pf : Expr) : MetaM (Expr × Array LMVarId) := do
  forallTelescopeReducing (← inferType pf) fun xs _ => do
    let pf := mkAppN pf xs
    let handlers ← kernelreassocImplRef.get
    let (pf, levels) ← handlers.firstM (fun h => h pf) <|> do
      throwError "`kernel_reassoc` can only be used on terms about equality of s-finite kernels."
    return (← mkLambdaFVars xs pf, levels)

end