Junyan Xu

Starting working on the new approach again ...

See my [latest commit](https://github.com/leanprover-community/mathlib4/commit/95679ab88fe0a67a2e5cb8e547f1d6eaeb50aae7) for more details.

Pushed another commit and I think you can handle the rest! Getting back to my own PRs ...

@Multramate Have you tried to clean up the rest of my branch? If not, I'll try to see if I can golf the subsequent computations today.

Thanks! [Here](https://github.com/leanprover-community/mathlib4/commit/ab3feb84d91f43a7ec55ef93a28e396e71e907b3) are some slight golf and a rephrase of the vector space result: ``` theorem Subspace.exists_eq_top_of_biUnion_eq_univ (hcovers : ⋃ p ∈ s, (p : Set E) = Set.univ) :...

I'm trying to use the equational criterion in the proof of https://stacks.math.columbia.edu/tag/00NZ, but it doesn't apply directly due to universe non-polymorphism. I'd like to take over this PR if no...

Thanks! Opened #20452.

Nice, the cache error finally goes away.

Thanks, LGTM!

GlueData' is indeed useful; my [GlueData.mk₂](https://github.com/leanprover-community/mathlib4/pull/14167/files#diff-84f8c7bdded56b516d33e74834faf603f2a1cc1c213351b2f10f72a851b94cfcR78-R96) is a baby version of it. But maybe we can add the `i ≠ j` conditions to `V, f, f_mono, f_hasPullback, t, t', t_fac`...