α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : 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 α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : y ∈ support (swap x (↑f x) * f)
⊢ y ∈ support f ∧ y ≠ x
simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : 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 α
inst✝ : Fintype α
f g : 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 α
inst✝ : Fintype α
f g : 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 α
inst✝ : Fintype α
f g : 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]
case neg.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f x = x
heq : y = x
hy : x ≠ x
⊢ ↑f x ≠ x ∧ x ≠ x

case neg.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : 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 hf heq <;>
simp_all only [not_true]
case neg.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
case neg.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f x = x
heq : y = x
hy : x ≠ x
⊢ ↑f x ≠ x ∧ x ≠ x

case neg.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
exact ⟨h, hy⟩
no goals
case neg.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
refine' ⟨hy, heq⟩