Commit 2026-10-14 22:05 66233bcf
View on Github →chore(Data/Vector/Basic): remove defeq abuse (#41095) This PR fixes* defeq abuse in Vector/Basic mainly by rewriting certain terms more carefully (i.e. first unfolding definition). *All but one of the original fixes now happened automatically in #41136 (automatically), but probably my versions of the proof are still cleaner over all. The one still saved set_option comes from replacing Subtype.mk_eq_mk with congr for a messy subtype.