ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
hy : y ∈ support (cycleOf f x)
⊢ y ∈ support f
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ support (cycleOf f x) ≤ support f
intro y hy
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
hy : (if SameCycle f x y then ↑f y else y) ≠ y
⊢ y ∈ support f
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
hy : y ∈ support (cycleOf f x)
⊢ y ∈ support f
rw [mem_support, cycleOf_apply] at hy
case inl
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h✝ : SameCycle f x y
hy : ↑f y ≠ y
⊢ y ∈ support f

case inr
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h✝ : ¬SameCycle f x y
hy : y ≠ y
⊢ y ∈ support f
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
hy : (if SameCycle f x y then ↑f y else y) ≠ y
⊢ y ∈ support f
split_ifs  at hy
no goals
case inl
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h✝ : SameCycle f x y
hy : ↑f y ≠ y
⊢ y ∈ support f
exact mem_support.mpr hy
no goals
case inr
ι : Type ?u.2513584
α : Type u_1
β : Type ?u.2513590
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h✝ : ¬SameCycle f x y
hy : y ≠ y
⊢ y ∈ support f
exact absurd rfl hy