Is there any shortening?

Stream: Is there code for X?

[Elif Uskuplu]

This can be a bit too much to ask, but I have a question about the following working example lean file. It's compiling but I think there may be shorter ways to get same results. I just wonder if there are some tactics that can shrink some lines. Thanks in advance if anyone has the time to take a look.

Justification.lean

[Aaron Liu]

This looks like defining free CABAs?

[Aaron Liu]

why aren't you using Set?

[Elif Uskuplu]

Good Question, thanks! I just wrote it today to get the result in the picture. It can be used to create an adjoint between SET and CABA. I can do everything in Set later, but I wonder if there are some unnecessarily long proofs in the file.
Screenshot from 2025-11-16 20-38-01.png

[Aaron Liu]

By Set I don't mean the category of sets but docs#Set (what most set-theorists would call the powerset), which has support for e.g. membership notation and set-builder notation

[Elif Uskuplu]

I see what you mean. Since every CABA is isomorphic to a Power Set algebra, I can apply the same approach in formalization. Probably better in my case. However, I'm still curious about the current proofs. Especially, in the proof of CabaHom_eq_of_agree_on_ι I think there may be some shorter way so to avoid some congr tactics. Some of the current proofs seem very ugly to me :) that's why I'm looking for suggestions :)