Commit 2024-07-24 18:12 43b64af1
View on Github →fix(Tactic/Simps): Prevent simps from viewing field_1 as a prefix of field. (#15095)
Related zulip thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Custom.20name.20for.20projection.20in.20.60structure.20extends.60