case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f = 1
⊢ card (support f) ≠ 1

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ¬f = 1
⊢ card (support f) ≠ 1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) ≠ 1
by_cases h : f = 1
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f = 1
⊢ card (support f) ≠ 1
exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one
no goals
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ¬f = 1
⊢ card (support f) ≠ 1
exact ne_of_gt (one_lt_card_support_of_ne_one h)