α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : Fintype αˣ
⊢ card α = card { a // a ≠ 0 } + Nat.succ 0
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : Fintype αˣ
⊢ card αˣ = card α - 1
rw [eq_comm, Nat.sub_eq_iff_eq_add (Fintype.card_pos_iff.2 ⟨(0 : α)⟩),
  Fintype.card_congr (unitsEquivNeZero α)]
no goals
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : Fintype αˣ
this : card α = card ({ a // a = 0 } ⊕ { a // ¬a = 0 })
⊢ card α = card { a // a ≠ 0 } + Nat.succ 0
rwa [Fintype.card_sum, add_comm, Fintype.card_subtype_eq] at this