α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
⊢ (if
        (if (if n = y then z else if n = z then y else n) = x then y
          else
            if (if n = y then z else if n = z then y else n) = y then x
            else if n = y then z else if n = z then y else n) =
          y then
      z
    else
      if
          (if (if n = y then z else if n = z then y else n) = x then y
            else
              if (if n = y then z else if n = z then y else n) = y then x
              else if n = y then z else if n = z then y else n) =
            z then
        y
      else
        if (if n = y then z else if n = z then y else n) = x then y
        else
          if (if n = y then z else if n = z then y else n) = y then x
          else if n = y then z else if n = z then y else n) =
    if n = z then x else if n = x then z else n
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
⊢ ↑(swap y z * swap x y * swap y z) n = ↑(swap z x) n
simp only [swap_apply_def, Perm.mul_apply]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
⊢ (if
        (if (if n = y then z else if n = z then y else n) = x then y
          else
            if (if n = y then z else if n = z then y else n) = y then x
            else if n = y then z else if n = z then y else n) =
          y then
      z
    else
      if
          (if (if n = y then z else if n = z then y else n) = x then y
            else
              if (if n = y then z else if n = z then y else n) = y then x
              else if n = y then z else if n = z then y else n) =
            z then
        y
      else
        if (if n = y then z else if n = z then y else n) = x then y
        else
          if (if n = y then z else if n = z then y else n) = y then x
          else if n = y then z else if n = z then y else n) =
    if n = z then x else if n = x then z else n
split_ifs <;> aesop