Trouble with sets

Stream: mathlib4

[Teddy Baker]

I am working on a problem that has to do with solving for the cardinality of a set. In order to solve the problem it is natural to construct maps onto new sets and show that the cardinality of the sets must agree. To do this, I have been mainly relying on Set.InjOn.encard_image and in the case where the sets are actually equal Set.ext. Although this works, it has been incredibly tedious to use Set.InjOn.encard_image, as it first requires proving the InjOn property, and then proving that the image of the map is indeed the desired set, which involves using Set.ext to prove equality of the sets. For each step, I generally have to unpack all of the different sets and then use all the membership functions, such as Set.mem_image and Set.mem_setOf or dsimp to finally arrive at the results, which tend to be repetitions of previously proved results.

I am wondering if there are any more powerful tools for this type of procedure, and whether there are higher level tactics that can be used to shorten this process. Schematically the process looks like this

have f_inj : Set.InjOn f set_a ∧ f '' set_a = set_b := by
    -- generally long and complicated proof here
card_eq := Set.InjOn.encard_image f_inj

In one problem, I had a series of set equivalences that compose to give the final answer, and each proof ends up being about a hundred lines, for what generally ends up being a rather simple set equivalence. Any help with the general strategy for this type of proof would be appreciated!

[Yaël Dillies]

Are your sets finite?

[Yaël Dillies]

Also I think this rather belongs in #mathlib4 or #general

[Notification Bot]

This topic was moved here from #lean4 > Trouble with sets by Scott Morrison.

[Teddy Baker]

The sets are finite but I have to prove they are finite, which is part of the process of proving the various set equivalences, therefore I have to use methods that are not only tailored for finite sets. I'm looking for a tactic kind of like congr for working with sums, or something of that nature. I'm also wondering if I'm going about it the best way. If this type of tool doesn't exist, that's ok too, I just want to make sure that I'm not missing an easier way to do things.

[Yaël Dillies]

If your sets are finite, I would highly advise you use Finset. Can you give us more context? ie click here :point_right: #mwe