no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a b x y : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ a ∈ {a, b}
simp
no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a b x y : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ b ∈ {a, b}
simp
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a b x✝ y✝ : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ SameCycle (swap a b) x y
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a b x✝ y✝ : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x ∈ {a, b}
y : α
hy : y ∈ {a, b}
⊢ SameCycle (swap a b) x y
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
case inl.inl
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
b x y✝ : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ SameCycle (swap y b) y y

case inl.inr
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ SameCycle (swap x y) x y

case inr.inl
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ SameCycle (swap y x) x y

case inr.inr
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a x y✝ : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ SameCycle (swap a y) y y
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a b x✝ y✝ : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ SameCycle (swap a b) x y
obtain rfl | rfl := hx <;> obtain rfl | rfl := hy
no goals
case inl.inl
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
b x y✝ : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ SameCycle (swap y b) y y
exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩
no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
b x y✝ : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ ↑(swap y b ^ 0) y = y
rw [zpow_zero, coe_one, id.def]
no goals
case inl.inr
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ SameCycle (swap x y) x y
exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ ↑(swap x y ^ 1) x = y
rw [zpow_one, swap_apply_left]
no goals
case inr.inl
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ SameCycle (swap y x) x y
exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
x✝ y✝ : α
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ ↑(swap y x ^ 1) x = y
rw [zpow_one, swap_apply_right]
no goals
case inr.inr
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a x y✝ : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ SameCycle (swap a y) y y
exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩
no goals
ι : Type ?u.1649642
α : Type u_1
β : Type ?u.1649648
f g : Perm α
s t : Set α
a x y✝ : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ ↑(swap a y ^ 0) y = y
rw [zpow_zero, coe_one, id.def]