ι : Type ?u.3061128
α : Type u_1
β : Type ?u.3061134
inst✝² : DecidableEq α
inst✝¹ : Fintype α
σ✝ τ : Perm α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < card (filter (fun x => ¬↑σ x = x) univ)
ι : Type ?u.3061128
α : Type u_1
β : Type ?u.3061134
inst✝² : DecidableEq α
inst✝¹ : Fintype α
σ✝ τ : Perm α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ card (filter (fun x => ↑σ x = x) univ) < Fintype.card α - 1
rw [lt_tsub_iff_left, ← lt_tsub_iff_right, ← Finset.card_compl, Finset.compl_filter]
no goals
ι : Type ?u.3061128
α : Type u_1
β : Type ?u.3061134
inst✝² : DecidableEq α
inst✝¹ : Fintype α
σ✝ τ : Perm α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < card (filter (fun x => ¬↑σ x = x) univ)
exact one_lt_card_support_of_ne_one h