porting pushforward_family

Stream: mathlib4

[Kevin Buzzard]

I'm porting the definition docs#category_theory.cover_dense.types.pushforward_family . A little before it in the file there's an include H which includes a hypothesis (H : CoverDense K G) which is almost always going to be there in practice but is not actually needed in the definition, and of course Lean 4 spots this because the hypothesis is not included in the definition in the ported file, and now I have a whole bunch of broken uses of this function because they're all including this superfluous H.

If I do nothing, i.e. remove H from the definition, then this will change the type of the declaration which of course might in theory give rise to problems later on, but in fact this declaration is only ever used in this file (this file isn't a leaf, it's imported in algebraic geometry, but the declaration itself is never used). Keeping the type of the declaration exactly how it is in mathlib3 will involve stating many of the variables used in it as inputs to the definition (to keep things in the right order; there are many variables declared after the include) but of course this is not the end of the world. I'm just wondering whether I really need to do this though. I'm tempted instead to let Lean 4 just tell me where I need H and where I don't, this sounds like a better solution to me. Is this within the bounds of a sensible idea?

[Eric Wieser]

Have you tried removing H from the def in mathlib3 and seeing what breaks?

[Kevin Buzzard]

Nothing breaks at all: #19002 . @Andrew Yang or @Adam Topaz do you have any comments about this change in the definition of pushforward_family? We no longer assume CoverDense K G. I propose porting the file in this form.

[Johan Commelin]

If is passes CI, please kick it on the queue (-;

[Kevin Buzzard]

It built locally.

[Adam Topaz]

LGTM!

[Kevin Buzzard]

@Johan Commelin just a heads-up: I realised that by actually just using include and omit precisely when H was needed I could keep the exact order of the inputs, so I pushed some more. Let's see if it compiles (it should do)