omega's Justification value

Stream: lean4

[Joachim Breitner]

I was trying to undersand omega better and wanted to define a Justificationbased on the pretty-printed trace output:

import Lean

set_option trace.omega true
theorem foo (h : x ≥ 3) (_ : y ≥ 5) : x + y ≥ 8 := by omega

/- includes:

[omega] Justification:
    [0, 1] ∈ ∅: combination of:
    • [0, 1] ∈ (-∞, 4]: tidying up:
      • [0, -1] ∈ [-4, ∞): 1 * x + -1 * y combo of:
        • [1] ∈ [3, ∞): assumption 0
        • [1, 1] ∈ (-∞, 7]: tidying up:
          • [-1, -1] ∈ [-7, ∞): assumption 4
    • [0, 1] ∈ [5, ∞): assumption 2
-/

open Lean.Omega
open Lean.Elab.Tactic.Omega

def justification : Justification ⟨.some 5, .some 4⟩ [0,1] :=
  Justification.combine
    (.tidy
      (.combo
         1
        (.assumption ⟨.some 3, .none⟩ [1] 0)
        (-1)
        (.tidy
          (.assumption ⟨.some (-7), .none⟩ [-1, -1] 4)))
    )
    (.assumption ⟨.some 5, .none⟩ [0,1] 2)

But the type checker doesn’t like it and I do not understand why:

application type mismatch
  (Justification.combo 1 (Justification.assumption { lowerBound := some 3, upperBound := none } [1] 0) (-1)
          (Justification.assumption { lowerBound := some (-7), upperBound := none } [-1, -1] 4).tidy).tidy.combine
    (Justification.assumption { lowerBound := some 5, upperBound := none } [0, 1] 2)
argument
  Justification.assumption { lowerBound := some 5, upperBound := none } [0, 1] 2
has type
  Justification { lowerBound := some 5, upperBound := none } [0, 1] : Type
but is expected to have type
  Justification { lowerBound := some 5, upperBound := none }
    (tidyCoeffs
      (Constraint.combo 1 { lowerBound := some 3, upperBound := none } (-1)
        (tidyConstraint { lowerBound := some (-7), upperBound := none } [-1, -1]))
      (Coeffs.combo 1 [1] (-1) (tidyCoeffs { lowerBound := some (-7), upperBound := none } [-1, -1]))) : Type

The tidyCoeffs expression here, presumably the bit that’s not matching, does reduce to [0,1], according to #reduce.

Did I just make a stupid typo here, or what might be going wrong here?