!4#3204 simps bug (Grothendieck construction)

Stream: PR reviews

[Scott Morrison]

@Floris van Doorn, in !4#3204, @[simps] is incorrectly producing lemmas for Prop-valued projections. I can't find the spot in the implementation of simp where it is meant to be discarding these, so I haven't fixed it. Would you be able to take a look at this?

[Floris van Doorn]

For fields that are sometimes propositions and sometimes not, @[simps] for now always generates this lemma. I can add a check that also checks whether the equality is propositional just before generating the simp lemma.
(the check for propositional fields is in the code for initialize_simps_projections)

[Scott Morrison]

Seems nice to do, otherwise this is a weird cause of simpNF linting errors, which are a pain to diagnose/review.

[Scott Morrison]

@Floris van Doorn, I guess a separate request about simp: could we have a way to say "produce all projects except the following", e.g. something like @[simps -inverse_map_fiber_down_down]. When there is just one to remove it is annoying to have to read through the output of @[simps?], and collecting the complement! Also hard to understand afterwards.