Module.Flat.of_shrink

Stream: mathlib4

[Andrew Yang]

docs#Module.Flat.of_shrink seems like a bad instance. My machine is currently trying to find

Module.Flat R (Shrink.{max (max (max (max u_2 ?u.793403) ?u.793404) ?u.793405) ?u.793406,
          max (max (max u_2 ?u.791045) ?u.791046) ?u.791047}
        (Shrink.{max (max (max u_2 ?u.791045) ?u.791046) ?u.791047, max (max u_2 ?u.789311) ?u.789312}
          (Shrink.{max (max u_2 ?u.789311) ?u.789312, max u_2 ?u.788243} (Shrink.{max u_2 ?u.788243, u_2} M))))

when the target is Module.Flat R M.

I'll open a PR to de-instance it if this is the case.

[Andrew Yang]

(and also docs#Module.Flat.of_ulift)

[Yaël Dillies]

Agreed! Those instances should probably go the other way around

[Kevin Buzzard]

shrink.png
Someone needs to shrink the docs too!

[Eric Wieser]

I remember seeing that ages ago, you should probably report on github since it's unsearchable on Zulip

[Andrew Yang]

Voila: #18537

[Kevin Buzzard]

and https://github.com/leanprover/doc-gen4/issues/226