no goals
ι : Type ?u.409761
α : Type u_1
β : Type ?u.409767
f g : Perm α
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ ↑(swap x y) y ≠ y
rwa [swap_apply_right]
ι : Type ?u.409761
α : Type u_1
β : Type ?u.409767
f g : Perm α
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
ι : Type ?u.409761
α : Type u_1
β : Type ?u.409767
f g : Perm α
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ ↑(swap x y ^ 1) y = a
rw [zpow_one, swap_apply_def]
no goals
ι : Type ?u.409761
α : Type u_1
β : Type ?u.409767
f g : Perm α
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
split_ifs at * <;> tauto