This is a junk theorem, it's trying to prove something that will sound strange or meaningless but is technically allowed by the details of the foundations.

Here it's building a list with one element and saying all elements of this list are equivalent. S̶o̶ ̶t̶h̶e̶ ̶f̶o̶l̶l̶o̶w̶i̶n̶g̶ ̶e̶l̶e̶m̶e̶n̶t̶s̶ ̶o̶f̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶ ̶a̶r̶e̶ ̶a̶l̶l̶ ̶e̶q̶u̶i̶v̶a̶l̶e̶n̶t̶ ̶t̶o̶ ̶e̶a̶c̶h̶ ̶o̶t̶h̶e̶r̶ ̶(̶t̶h̶e̶r̶e̶ ̶i̶s̶ ̶a̶ ̶s̶i̶n̶g̶l̶e̶ ̶e̶l̶e̶m̶e̶n̶t̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶)̶

It doesn't mean anything. The point is that the language of lean, and its proof derivation system, are able to express (and prove) statements that do not correspond to any meaningful mathematics.

As I think another commenter hinted, the binary expansion of 7 is 111. And indeed, 1 = 1 = 1

List.TFAE is a helper definition and it’s invoked on a funny looking term when translated directly into english. I don’t know what I think, yeah it’s kinda junky but not in the way that 57 \mem 100 in a set encoding of the naturals.

    theorem TFAE_7_binary : List.TFAE (7).bits := by
  unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!

The following are equivalent: