Mapping iff

Stream: Is there code for X?

[Waelwindows]

Hello, i'm trying to prove a theorem, and i've reached a stage where I have to prove a = b <-> b = a.
How do I apply symm only to one side of the iff?

Here's the theorem I'm trying to prove

import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.GroupPower.Basic

variable {G : Type*} [Group G]
variable (a b c : G)

example : (a*b)^2 = a^2*b^2 ↔ a*b=b*a := by
  rw [pow_two, pow_two, pow_two] -- fully expand
  rw [mul_assoc, mul_assoc]
  rw [← mul_assoc b a b, ← mul_assoc a b b]
  rw [mul_left_cancel_iff, mul_right_cancel_iff]

[Ruben Van de Velde]

Eq.symm is an implication, so you could split your goal into the two directions and then apply it

[Ruben Van de Velde]

But we also have eq_comm which you can rw with

[Waelwindows]

Thank you, eq_comm is exactly what I wanted.

Ruben Van de Velde said:

Eq.symm is an implication, so you could split your goal into the two directions and then apply it

How can I split the goal in this case?

[Ruben Van de Velde]

constructor

[Kevin Buzzard]

Note that in general you can't apply an implication P -> Q to one side of an iff P <-> R, because the resulting goal Q <-> R might be true in cases where the original goal P <-> R is false. This shows that it's not just a case of figuring out how to do what you asked to do, you really need eq_comm. The symm tactic works fine with just implications.

[Eric Rodriguez]

On the other hand, you don't need to rewrite - you can also say that this is exactly the theorem eq_comm; i.e. exact eq_comm.