case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
cases' eq_zero_or_neZero p with hp hp
no goals
case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1
case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1
subst hp
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1
simp only [ZMod, not_prime_zero, false_iff_iff, zero_tsub]
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0
suffices Fintype.card ℤˣ ≠ 0 by convert this
no goals
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0
simp
no goals
inst✝ : Fintype (ZMod 0)ˣ
this : Fintype.card ℤˣ ≠ 0
⊢ ¬Fintype.card ℤˣ = 0
convert this