Junyan Xu

I can't quite fit it into the lemmas I introduced for the case of fp modules, but I was able to [golf down the proof a bit](https://github.com/leanprover-community/mathlib/compare/finite_presentation_of_comp...alreadydone:mathlib:finite_presentation_of_comp?expand=1) using quotient ring...

Update: I'm now able to adapt the proof to make use of my lemmas, but unfortunately [the proof becomes longer](https://github.com/leanprover-community/mathlib/commit/13acb1ae10e8690304ae932bf685a3764f7bed56); I also need an additional lemma that says AX is...

still not compatible though everything has switched to WE ...

OK. I can keep using TST but is there an option to disable tree structure completely? All other vertical/sidebar tab add-ons don't currently support Multiple Tab Handler. I mainly use...

> Is there a way to accept all the suggestions in one go? You should see an "add suggestion to batch" button, and you may commit them together.

Thanks! > For instance (h : S.objs.nonempty) : nonempty S.coe := ⟨⟨h.some,h.some_spec⟩⟩ , the linter is also unhappy with this because it says: Indeed it shouldn't be an instance. You...

Hi @bottine I've simplified some proofs over in [my fork](https://github.com/leanprover-community/mathlib/compare/bottine/subgroupoid...alreadydone:mathlib:bottine/subgroupoid?expand=1) and pointed out most notable changes as comments here. Notice that I haven't merged your latest commit. Mostly I golf...

Thanks! maintainer merge (or delegate and wait for CI, but note that queue is empty now)

I just observed `wlog` generating a buggy proof that the kernel rejects: it's the proof of `pow_eq_one_of_norm_eq_one` [here](https://github.com/leanprover-community/mathlib/compare/top_alg_poly_golf...num_field_embeddings_golf?expand=1#diff-c9ef3c1ed37ddbba77b03f93db13937b9369ed5e9a322c197de9441f2a4e5c61R131). This is with the `wlog` currently in mathlib, so this bug may...

Beware that the last commit would conflict with [#16804](https://github.com/leanprover-community/mathlib/pull/16804/files#diff-c9ef3c1ed37ddbba77b03f93db13937b9369ed5e9a322c197de9441f2a4e5c61R111-R120) where I used a trick to replace the buggy `wlog`. (I suspect the trick is pretty widely applicable and actually may...