case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ p = 1 ↔ Nat.Prime p

case prime
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ p = q ↔ Nat.Prime p
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p
cases' hq with q hq_one hq_prime hq_hchar
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ p = 1 ↔ Nat.Prime p
rw [(CharP.eq R hp inferInstance : p = 0)]
no goals
case zero
R : Type u
inst✝ : Semiring R
p : ℕ
hp : CharP R p
q : CharZero R
⊢ 0 = 1 ↔ Nat.Prime 0
decide
no goals
case prime
R : Type u
inst✝ : Semiring R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hq_hchar : CharP R q
⊢ p = q ↔ Nat.Prime p
exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp hq_hchar⟩