[GOAL]
α : Type u_1
x : ℤˣ
⊢ x ∈ {1, -1}
[PROOFSTEP]
cases Int.units_eq_one_or x
[GOAL]
case inl
α : Type u_1
x : ℤˣ
h✝ : x = 1
⊢ x ∈ {1, -1}
[PROOFSTEP]
simp [*]
[GOAL]
case inr
α : Type u_1
x : ℤˣ
h✝ : x = -1
⊢ x ∈ {1, -1}
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α = card αˣ + 1
[PROOFSTEP]
rw [eq_comm, Fintype.card_congr (unitsEquivNeZero α)]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card { a // a ≠ 0 } + 1 = card α
[PROOFSTEP]
have := Fintype.card_congr (Equiv.sumCompl (· = (0 : α)))
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) = card α
⊢ card { a // a ≠ 0 } + 1 = card α
[PROOFSTEP]
rwa [Fintype.card_sum, add_comm, Fintype.card_subtype_eq] at this 
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
have : Fintype α := Fintype.ofFinite α
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
classical rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_eq_card_units_add_one]
[GOAL]
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = Nat.card αˣ + 1
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, Fintype.card_eq_card_units_add_one]
[GOAL]
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card αˣ = card α - 1
[PROOFSTEP]
rw [@Fintype.card_eq_card_units_add_one α, Nat.add_sub_cancel]
