α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ cycleType f ≤ cycleType g
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
⊢ cycleType f ≤ cycleType g
have hf' := mem_cycleFactorsFinset_iff.1 hf
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ map (Finset.card ∘ support) {f}.val ≤ map (Finset.card ∘ support) (cycleFactorsFinset g).val
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ cycleType f ≤ cycleType g
rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ {f}.val ≤ (cycleFactorsFinset g).val
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ map (Finset.card ∘ support) {f}.val ≤ map (Finset.card ∘ support) (cycleFactorsFinset g).val
refine map_le_map ?_
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ cycleFactorsFinset g
hf' : IsCycle f ∧ ∀ (a : α), a ∈ support f → ↑f a = ↑g a
⊢ {f}.val ≤ (cycleFactorsFinset g).val
simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf