ι : Type ?u.2746614
α : Type u_1
β : Type ?u.2746620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ p f : Perm α
h : IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
⊢ support p ≤ support f
ι : Type ?u.2746614
α : Type u_1
β : Type ?u.2746620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ p f : Perm α
h : p ∈ cycleFactorsFinset f
⊢ support p ≤ support f
rw [mem_cycleFactorsFinset_iff] at h
ι : Type ?u.2746614
α : Type u_1
β : Type ?u.2746620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ p f : Perm α
h : IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
x : α
hx : x ∈ support p
⊢ x ∈ support f
ι : Type ?u.2746614
α : Type u_1
β : Type ?u.2746620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ p f : Perm α
h : IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
⊢ support p ≤ support f
intro x hx
no goals
ι : Type ?u.2746614
α : Type u_1
β : Type ?u.2746620
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ p f : Perm α
h : IsCycle p ∧ ∀ (a : α), a ∈ support p → ↑p a = ↑f a
x : α
hx : x ∈ support p
⊢ x ∈ support f
rwa [mem_support, ← h.right x hx, ← mem_support]