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

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Perm α)
inst✝ : DecidableEq α
σ : Perm α
h : IsSwap σ
⊢ _root_.orderOf σ = 2
Tactic:
rw [← Equiv.Perm.lcm_cycleType, h.cycleType, Multiset.lcm_singleton, normalize_eq]
State after:
no goals