α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : ↑(swap x (↑f x) * f) y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
by_cases h : f y = x
no goals
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
constructor <;> intro <;> simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
no goals
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
split_ifs at hy with h h <;> try { subst x } <;> try { simp [*] at * }