`kernelReassocHandler`🔗

Definition

Core handler for @[kernel_reassoc].

Given an equality between s-finite kernels, this constructs the corresponding reassociated equality in SFinKer category, under the extra Z measurable space and instance binders needed to state the result. The returned array contains the fresh level metavariables that still need to be added to the declaration's universe levels.

def

kernelReassocHandler (h_eq : Lean.Expr) :
  Lean.MetaM (Lean.Expr × Array Lean.LMVarId)
kernelReassocHandler (h_eq : Lean.Expr) :
  Lean.MetaM
    (Lean.Expr × Array Lean.LMVarId)

Code

def kernelReassocHandler (h_eq : Expr) : MetaM (Expr × Array LMVarId) := do
  let eq_type ← inferType h_eq
  let some (_, lhs, _) := eq_type.eq? |
    throwError "Expected an equality, but got {eq_type}"
  let (_, Y, _, _) ← getTypesFromKernel lhs
  let u ← mkFreshLevelMVar
  let proof : Expr ←
    withLocalDecl `Z .implicit (mkSort (mkLevelSucc u)) fun Z => do
      let mspaceType ← mkAppM ``MeasurableSpace #[Z]
      withLocalDecl `inst .instImplicit mspaceType fun _inst => do
        let kernelType ← mkAppMInst ``Kernel #[Y, Z] 2
        withLocalDeclD `ξ kernelType fun ξ => do
          let sfiniteType ← mkAppM ``IsSFiniteKernel #[ξ]
          withLocalDecl `inst_1 BinderInfo.instImplicit sfiniteType fun _inst_1 => do
            let (_, hom_proof) ← HomEqualityToLvl eq_type u
            let hom_proof ← mkAppM ``Eq.mp #[hom_proof, h_eq]
            let (hom_proof_reassoc, _) ← reassocExprHom hom_proof
            let univs ← collectExprUniverses eq_type
            let maxLvl ← computeMaxLevel <| u :: univs
            let (ξ_lift, _) ← liftKernel ξ maxLvl []
            let (ξ_hom, _) ← transformKernelToHom ξ_lift []
            let reassoc_body ← mkAppM' hom_proof_reassoc #[ξ_hom]
            let (_, kernel_reassoc_proof) ← KernelEquality <| ← inferType reassoc_body
            let kernel_reassoc_proof ← mkAppM ``Eq.mp #[kernel_reassoc_proof, reassoc_body]
            mkLambdaFVars #[Z, _inst, ξ, _inst_1] kernel_reassoc_proof
  let proof ← freshenLevelParam proof
  return (proof, #[u.mvarId!])

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 26 project declarations, 230 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

kernelReassocHandler🔗

`kernelReassocHandler`🔗