ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y =
    if SameCycle f x y then ↑f y else y
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ ↑(cycleOf f x) y = if SameCycle f x y then ↑f y else y
dsimp only [cycleOf]
case inl
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : SameCycle f x y
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y = ↑f y

case inr
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : ¬SameCycle f x y
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y = y
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y =
    if SameCycle f x y then ↑f y else y
split_ifs with h
case inl.ha
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : SameCycle f x y
⊢ SameCycle f x y
case inl
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : SameCycle f x y
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y = ↑f y
apply ofSubtype_apply_of_mem
no goals
case inl.ha
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : SameCycle f x y
⊢ SameCycle f x y
exact h
case inr.ha
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : ¬SameCycle f x y
⊢ ¬SameCycle f x y
case inr
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : ¬SameCycle f x y
⊢ ↑(↑ofSubtype (subtypePerm f (_ : ∀ (x_1 : α), SameCycle f x x_1 ↔ SameCycle f x (↑f x_1)))) y = y
apply ofSubtype_apply_of_not_mem
no goals
case inr.ha
ι : Type ?u.2112614
α : Type u_1
β : Type ?u.2112620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y✝ : α
f : Perm α
x y : α
h : ¬SameCycle f x y
⊢ ¬SameCycle f x y
exact h