[Merged by Bors] - chore: add issue number to instance was not necessary porting notes#10671

pitmonticone wants to merge 1 commit intomasterleanprover-community/mathlib4:masterfrom

pitmonticone/instance-was-not-necessaryleanprover-community/mathlib4:pitmonticone/instance-was-not-necessaryCopy head branch name to clipboard