mathlib4#659

Stream: PR reviews

[Scott Morrison]

mathlib4#659 still has a few rough edges, which @Winston Yin has described in the PR. I haven't had a chance to have a look at them, and it would be great if we could get this PR moving again. I suspect it is on the critical path. If any mathlib4 porters could take a look and triage the remaining problems (i.e. say they are fine, or write up zulip posts with MWEs, etc) that would be great.

[Winston Yin]

Instance loop: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instance.20loop.3F/near/311533638
↑1 = 1: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.86.911.20.3D.201.3F/near/311798847
simp not using lemma: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/311227341