∀ (u v : Lean.Level),
  Lean.Meta.Sym.isLevelDefEqS✝ u v =
    match u, v with
    | Lean.Level.param u, Lean.Level.param v => pure (u == v)
    | Lean.Level.zero, Lean.Level.zero => pure true
    | u.succ, v.succ => Lean.Meta.Sym.isLevelDefEqS✝¹ u v
    | Lean.Level.zero, a.succ => pure false
    | a.succ, Lean.Level.zero => pure false
    | Lean.Level.zero, v₁.max v₂ =>
      Lean.Meta.Sym.isLevelDefEqS✝² Lean.Level.zero v₁ <&&> Lean.Meta.Sym.isLevelDefEqS✝³ Lean.Level.zero v₂
    | u₁.max u₂, Lean.Level.zero =>
      Lean.Meta.Sym.isLevelDefEqS✝⁴ u₁ Lean.Level.zero <&&> Lean.Meta.Sym.isLevelDefEqS✝⁵ u₂ Lean.Level.zero
    | Lean.Level.zero, a.imax v => Lean.Meta.Sym.isLevelDefEqS✝⁶ Lean.Level.zero v
    | a.imax u, Lean.Level.zero => Lean.Meta.Sym.isLevelDefEqS✝⁷ u Lean.Level.zero
    | u₁.max u₂, v₁.max v₂ => Lean.Meta.Sym.isLevelDefEqS✝⁸ u₁ v₁ <&&> Lean.Meta.Sym.isLevelDefEqS✝⁹ u₂ v₂
    | u₁.imax u₂, v₁.imax v₂ => Lean.Meta.Sym.isLevelDefEqS✝¹⁰ u₁ v₁ <&&> Lean.Meta.Sym.isLevelDefEqS✝¹¹ u₂ v₂
    | x, x_1 => Lean.Meta.Sym.tryAssignLevelMVar✝ u v <||> Lean.Meta.Sym.tryAssignLevelMVar✝¹ v u