Commit 2026-02-09 08:58 d16c7456

chore(style): fix more duplicate instances (#35006) This PR fixes instances of duplicate instances appearing in the local context that require movements of source code (to adjust which variables are visible). Note that, like #35002, it does not adjust resulting types. (It does tweak one proof in Mathlib.LinearAlgebra.Ray while we're at it.) This is motivated by the upcoming overlapping instances linter, which fires on duplicate instances in the local context (even if these do not appear in the resulting definition's type). See also this Zulip thread for discussion on removing duplicate instances.