eq_comm with implicit args

Stream: general

[Yakov Pechersky]

Is it possible to either redefine eq_comm or provide another version that is like:

lemma eq_comm {α : Sort u} ⦃a b : α⦄ : a = b ↔ b = a :=
⟨eq.symm, eq.symm⟩

Often, I have to rely on eq_comm to rearrange some equalities so that iff statements like docs#map_eq_some' can actually proc. Alternatively, suggestions on how to get such iffs to simp when the equality is in the RHS = LHS form would be welcome.

[Mario Carneiro]

Is it so bad to write @eq_comm _?

[Mario Carneiro]

I don't understand your example use case

[Yakov Pechersky]

No, it's not so bad.

[Chris Hughes]

I agree that they should be explicit arguments, but I don't feel very strongly about it.

[Yury G. Kudryashov]

lemma eq_comm' {α : Sort u} (a b : α) : a = b ↔ b = a := eq_comm

[Yury G. Kudryashov]

In some cases I added symmetric versions of simp lemmas.