mathlib

37ab34ea - doc(tactic/congr): example where congr fails, but exact works (#7208)

doc(tactic/congr): example where congr fails, but exact works (#7208) As requested on zulip: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.237084/near/234652967