`BookProof.ChapterAttentionMasking.mem_causalMask` {i l : Fin m} : l ∈ causalMask m i ↔ l ≤ i

Initializing...

`BookProof.ChapterAttentionMasking.mem_causalMask` {i l : Fin m} : l ∈ causalMask m i ↔ l ≤ i · Prove2Me