Commit 2026-03-18 03:37 553b79e5

feat(Tactic/FastInstance): skip mkAuxTheorem for proof fields when types agree at instances transparency (#36717) This PR improves how `fast_instance%` handles proof-valued constructor fields. Previously, proof fields were always wrapped in `mkAuxTheorem`, which creates a separate auxiliary theorem carrying the expected type. This is unnecessary when the proof's actual type already agrees with the expected type at instances transparency — in that case the proof can be assigned directly. The new behaviour: check whether the proof's type agrees with the expected type at instances transparency. If yes, assign directly. If no (indicating a binder type mismatch), wrap with `mkAuxTheorem` as before. This is a natural analogue of the data-field binder type checking that `fast_instance%` already performs, applied to proof fields. 🤖 Prepared with Claude Code