doc: porting note on quotient ⟦a⟧ notation (#4306)

The details of this notation changed between mathlib 3 and 4, so we should leave a porting note about this change and give a bit motivation (the motivation is actually not totally clear anymore).

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/confusion.20between.20equivalence.20and.20instance.20setoid/near/360822354

Mathlib/Data/Quot.lean

@@ -216,6 +216,11 @@ variable [sa : Setoid α] [sb : Setoid β]
 
 variable {φ : Quotient sa → Quotient sb → Sort _}
 
+-- Porting note: in mathlib3 this notation took the Setoid as an instance-implicit argument,
+-- now it's explicit but left as a metavariable.
+-- We have not yet decided which one works best, since the setoid instance can't always be
+-- reliably found but it can't always be inferred from the expected type either.
+-- See also: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/confusion.20between.20equivalence.20and.20instance.20setoid/near/360822354
 @[inherit_doc]
 notation:arg "⟦" a "⟧" => Quotient.mk _ a