Theorem: Equiv.Perm.IsSwap.cycleType (Jordan/Jordan.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ Perm.cycleType σ = {2}
Tactic:
simp only [h.isCycle.cycleType, Equiv.Perm.card_support_eq_two.mpr h]
State after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ ↑[2] = {2}

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ ↑[2] = {2}
Tactic:
simp only [Multiset.coe_singleton]
State after:
no goals