case intro.intro.intro
ι : Type ?u.418035
α : Type u_1
β : Type ?u.418041
g : Perm α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hxy : x ≠ y
⊢ IsCycle (swap x y)
ι : Type ?u.418035
α : Type u_1
β : Type ?u.418041
f g : Perm α
x y : α
inst✝ : DecidableEq α
⊢ IsSwap f → IsCycle f
rintro ⟨x, y, hxy, rfl⟩
no goals
case intro.intro.intro
ι : Type ?u.418035
α : Type u_1
β : Type ?u.418041
g : Perm α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hxy : x ≠ y
⊢ IsCycle (swap x y)
exact isCycle_swap hxy