case ofNat
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ Int.ofNat a✝)
h2 : support f ⊆ support (f ^ Int.ofNat a✝)
⊢ IsCycle f

case negSucc
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ Int.negSucc a✝)
h2 : support f ⊆ support (f ^ Int.negSucc a✝)
⊢ IsCycle f
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℤ
h1 : IsCycle (f ^ n)
h2 : support f ⊆ support (f ^ n)
⊢ IsCycle f
cases n
no goals
case ofNat
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ Int.ofNat a✝)
h2 : support f ⊆ support (f ^ Int.ofNat a✝)
⊢ IsCycle f
exact h1.of_pow h2
case negSucc
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ (a✝ + 1))⁻¹
h2 : support f ⊆ support (f ^ (a✝ + 1))
⊢ IsCycle f
case negSucc
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ Int.negSucc a✝)
h2 : support f ⊆ support (f ^ Int.negSucc a✝)
⊢ IsCycle f
simp only [le_eq_subset, zpow_negSucc, Perm.support_inv] at h1 h2
no goals
case negSucc
ι : Type ?u.1087130
α : Type u_1
β : Type ?u.1087136
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : IsCycle (f ^ (a✝ + 1))⁻¹
h2 : support f ⊆ support (f ^ (a✝ + 1))
⊢ IsCycle f
exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2