Theorem: Equiv.perm_is_nontrivial (Jordan/Mathlib/GroupTheory/Subgroup/Basic.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 1 < Fintype.card α ↔ Nontrivial (Perm α)
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, Fintype.card_perm, Nat.one_lt_factorial]
State after:
no goals