[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
trans x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k)
[PROOFSTEP]
simp_rw [h.add_pow, ← Nat.Ico_zero_eq_range, Nat.Ico_succ_right, Icc_eq_cons_Ico (zero_le _), Finset.sum_cons,
  Ico_eq_cons_Ioo (pow_pos hp.pos _), Finset.sum_cons, tsub_self, tsub_zero, pow_zero, Nat.choose_zero_right,
  Nat.choose_self, Nat.cast_one, mul_one, one_mul, ← add_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ↑p * ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)
[PROOFSTEP]
simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n : ℕ
⊢ ∑ k in Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k) =
    ∑ x_1 in Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * ↑(Nat.choose (p ^ n) x_1 / p * p)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : i ∈ Ioo 0 (p ^ n)
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
[PROOFSTEP]
rw [mem_Ioo] at hi 
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
n i : ℕ
hi : 0 < i ∧ i < p ^ n
⊢ x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i) = x ^ i * y ^ (p ^ n - i) * ↑(Nat.choose (p ^ n) i / p * p)
[PROOFSTEP]
rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p : ℕ
x y : R
hp : Nat.Prime p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k in Ioo 0 p, x ^ k * y ^ (p - k) * ↑(Nat.choose p k / p)
[PROOFSTEP]
simpa using h.add_pow_prime_pow_eq hp 1
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ ↑(Fintype.card R) = 0
[PROOFSTEP]
rw [← nsmul_one, card_nsmul_eq_zero]
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : ℕ
⊢ ↑n = 0 ↔ addOrderOf 1 ∣ n
[PROOFSTEP]
rw [← Nat.smul_one_eq_coe, addOrderOf_dvd_iff_nsmul_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
rcases lt_trichotomy a 0 with (h | rfl | h)
[GOAL]
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
[GOAL]
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ -a
[PROOFSTEP]
lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
[PROOFSTEP]
rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
[GOAL]
case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0
[PROOFSTEP]
simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
[GOAL]
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a
[PROOFSTEP]
lift a to ℕ using le_of_lt h with b
[GOAL]
case inr.inr.intro
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
b : ℕ
h✝ h : 0 < ↑b
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
[PROOFSTEP]
rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
[PROOFSTEP]
rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]
[PROOFSTEP]
rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
[GOAL]
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
⊢ ↑↑a = ↑↑b ↔ a ≡ b [MOD p]
[PROOFSTEP]
exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x
[PROOFSTEP]
rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x
[PROOFSTEP]
rw [zero_dvd_iff]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
exact ⟨H x, by rintro rfl; simp⟩
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ x = 0 → ↑x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) = 0
⊢ ↑(x % Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0))) = 0
[PROOFSTEP]
rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add, Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul, add_zero] at H1 
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find (_ : ∃ x, ¬(↑x = 0 → x = 0)) ∣ x
⊢ ↑x = 0
[PROOFSTEP]
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul, of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
[PROOFSTEP]
letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).1
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
[PROOFSTEP]
exact CharP.cast_eq_zero_iff R (ringChar R)
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ↑(ringChar R) = 0
[PROOFSTEP]
rw [ringChar.spec]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p
[PROOFSTEP]
let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hp.out
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * r
⊢ (x + y) ^ p = x ^ p + y ^ p
[PROOFSTEP]
simp [hr]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
[PROOFSTEP]
let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hp.out n
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
[PROOFSTEP]
simp [hr]
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p
[PROOFSTEP]
rw [eq_sub_iff_add_eq, ← add_pow_char_of_commute _ _ _ (Commute.sub_left h rfl)]
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y + y) ^ p = x ^ p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
n : ℕ
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
n : ℕ
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
case zero
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ Nat.zero = x ^ p ^ Nat.zero - y ^ p ^ Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x - y) ^ p ^ Nat.zero = x ^ p ^ Nat.zero - y ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x - y) ^ p ^ Nat.succ n = x ^ p ^ Nat.succ n - y ^ p ^ Nat.succ n
[PROOFSTEP]

| succ n n_ih =>
  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
  apply sub_pow_char_of_commute; apply Commute.pow_pow h
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x - y) ^ p ^ Nat.succ n = x ^ p ^ Nat.succ n - y ^ p ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih]
[GOAL]
case succ
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ (x ^ p ^ n - y ^ p ^ n) ^ p = (x ^ p ^ n) ^ p - (y ^ p ^ n) ^ p
[PROOFSTEP]
apply sub_pow_char_of_commute
[GOAL]
case succ.h
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
n : ℕ
n_ih : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
⊢ Commute (x ^ p ^ n) (y ^ p ^ n)
[PROOFSTEP]
apply Commute.pow_pow h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ -1 ≠ 1
[PROOFSTEP]
suffices (2 : R) ≠ 0 by
  intro h
  symm at h 
  rw [← sub_eq_zero, sub_neg_eq_add] at h 
  norm_num at h 
  exact this h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
⊢ -1 ≠ 1
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h : -1 = 1
⊢ False
[PROOFSTEP]
symm at h 
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h : 1 = -1
⊢ False
[PROOFSTEP]
rw [← sub_eq_zero, sub_neg_eq_add] at h 
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h✝ : 1 = -1
h : 1 + 1 = 0
⊢ False
[PROOFSTEP]
norm_num at h 
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
this : 2 ≠ 0
h✝ : 1 = -1
h : 2 = 0
⊢ False
[PROOFSTEP]
exact this h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ 2 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : 2 = 0
⊢ False
[PROOFSTEP]
rw [show (2 : R) = (2 : ℕ) by norm_cast] at h 
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : 2 = 0
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
⊢ False
[PROOFSTEP]
have := (CharP.cast_eq_zero_iff R p 2).mp h
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this : p ∣ 2
⊢ False
[PROOFSTEP]
have := Nat.le_of_dvd (by decide) this
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this : p ∣ 2
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
h : ↑2 = 0
this✝ : p ∣ 2
this : p ≤ 2
⊢ False
[PROOFSTEP]
rw [fact_iff] at *
[GOAL]
R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : 2 < p
h : ↑2 = 0
this✝ : p ∣ 2
this : p ≤ 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p = -1
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p + 1 = 0
[PROOFSTEP]
nth_rw 2 [← one_pow p]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p + 1 ^ p = 0
[PROOFSTEP]
rw [← add_pow_char, add_left_neg, zero_pow (Fact.out (p := Nat.Prime p)).pos]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n = -1
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 = 0
[PROOFSTEP]
nth_rw 2 [← one_pow (p ^ n)]
[GOAL]
R : Type u_1
inst✝² : CommRing R
p n : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (Nat.Prime p)
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
[PROOFSTEP]
rw [← add_pow_char_pow, add_left_neg, zero_pow (pow_pos (Fact.out (p := Nat.Prime p)).pos _)]
[GOAL]
R : Type u_1
K : Type u_2
L : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Semiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p
[PROOFSTEP]
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, f.map_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
⊢ (↑(frobenius R p))^[n] x = x ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
⊢ (↑(frobenius R p))^[n] x = x ^ p ^ n
[PROOFSTEP]
induction n with
| zero => simp
| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
⊢ (↑(frobenius R p))^[Nat.zero] x = x ^ p ^ Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
⊢ (↑(frobenius R p))^[Nat.zero] x = x ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
n_ih : (↑(frobenius R p))^[n] x = x ^ p ^ n
⊢ (↑(frobenius R p))^[Nat.succ n] x = x ^ p ^ Nat.succ n
[PROOFSTEP]

| succ n n_ih => rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
n_ih : (↑(frobenius R p))^[n] x = x ^ p ^ n
⊢ (↑(frobenius R p))^[Nat.succ n] x = x ^ p ^ Nat.succ n
[PROOFSTEP]
rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H : ↑(frobenius R p) x = ↑(frobenius R p) h
⊢ x = h
[PROOFSTEP]
rw [← sub_eq_zero] at H ⊢
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) x - ↑(frobenius R p) h = 0
⊢ x - h = 0
[PROOFSTEP]
rw [← frobenius_sub] at H 
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x h : R
H✝ : ↑(frobenius R p) x = ↑(frobenius R p) h
H : ↑(frobenius R p) (x - h) = 0
⊢ x - h = 0
[PROOFSTEP]
exact IsReduced.eq_zero _ ⟨_, H⟩
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
⊢ IsSquare a
[PROOFSTEP]
cases nonempty_fintype R
[GOAL]
case intro
R✝ : Type u_1
R : Type u_2
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a
[PROOFSTEP]
exact
  Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
    (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = ↑(k % p + p * (k / p))
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑(k % p + p * (k / p)) = ↑(k % p)
[PROOFSTEP]
simp [cast_eq_zero]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False
[PROOFSTEP]
haveI : CharZero R := charP_to_charZero R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False
[PROOFSTEP]
cases nonempty_fintype R
[GOAL]
case intro
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
val✝ : Fintype R
⊢ False
[PROOFSTEP]
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))
[GOAL]
R : Type u_1
inst✝¹ inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R
[PROOFSTEP]
rw [ringChar.eq_iff, charP_zero_iff_charZero]
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p k m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
⊢ x ^ (p ^ Nat.zero * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
rw [pow_zero, one_mul]
[GOAL]
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
⊢ x ^ (p ^ Nat.succ k * m) = 1 ↔ x ^ m = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h : x ^ (p ^ Nat.succ k * m) = 1
⊢ x ^ m = 1
[PROOFSTEP]
rw [pow_succ, mul_assoc, pow_mul', ← frobenius_def, ← frobenius_one p] at h 
[GOAL]
case succ.refine'_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h✝ : ↑(frobenius R p) (x ^ (p ^ k * m)) = 1
h : ↑(frobenius R p) (x ^ (p ^ k * m)) = ↑(frobenius R p) 1
⊢ x ^ m = 1
[PROOFSTEP]
exact hk.1 (frobenius_inj R p h)
[GOAL]
case succ.refine'_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsReduced R
p m : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
x : R
k : ℕ
hk : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1
h : x ^ m = 1
⊢ x ^ (p ^ Nat.succ k * m) = 1
[PROOFSTEP]
rw [pow_mul', h, one_pow]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ 1 = 0
[PROOFSTEP]
simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p
[PROOFSTEP]
rw [‹e = p›] at hmul 
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p
[PROOFSTEP]
rw [one_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : NoZeroDivisors R
p : ℕ
hc : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = p
[PROOFSTEP]
exact Eq.symm hmul
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ r = 1 * r
[PROOFSTEP]
rw [one_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 1 * r = ↑1 * r
[PROOFSTEP]
rw [Nat.cast_one]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ ↑1 * r = 0 * r
[PROOFSTEP]
rw [CharP.cast_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 0 * r = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
this : ∀ (r : R), r = 0
a b : R
⊢ a = b
[PROOFSTEP]
rw [this a, this b]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ False
[PROOFSTEP]
apply zero_ne_one' R
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 0 = 1
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
h : ringChar R = 1
⊢ 1 = 0
[PROOFSTEP]
rw [← Nat.cast_one, ringChar.spec, h]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : ↑1 = 0
⊢ v = 1
[PROOFSTEP]
rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h 
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0
[PROOFSTEP]
rw [Ne.def, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)
[PROOFSTEP]
exact mt (or_iff_left hR).mp CharP.ringChar_ne_one
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
[PROOFSTEP]
have H : (n : R) = 0 := by rw [← hn, CharP.cast_card_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ↑n = 0
[PROOFSTEP]
rw [← hn, CharP.cast_card_eq_zero]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
[PROOFSTEP]
intro k
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 ↔ n ∣ k
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 → n ∣ k
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑k = 0
⊢ n ∣ k
[PROOFSTEP]
rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h 
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n ∣ k
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero]
[GOAL]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ k % n = 0
[PROOFSTEP]
apply hR _ (Nat.mod_lt _ _) h
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n > 0
[PROOFSTEP]
rw [← hn, gt_iff_lt, Fintype.card_pos_iff]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ Nonempty R
[PROOFSTEP]
exact ⟨0⟩
[GOAL]
case mpr
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ n ∣ k → ↑k = 0
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑(n * k) = 0
[PROOFSTEP]
rw [Nat.cast_mul, H, zero_mul]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain ⟨c, hc⟩ := CharP.exists R
[GOAL]
case intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
[PROOFSTEP]
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R c, ← hn, CharP.cast_card_eq_zero]
[GOAL]
case intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain ⟨i, hi, hc⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn 
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i, i ≤ n ∧ c = p ^ i
[PROOFSTEP]
rwa [Nat.dvd_prime_pow hp.1] at hcpn 
[GOAL]
case intro.intro.intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ CharP R (p ^ n)
[PROOFSTEP]
obtain rfl : i = n := by
  apply hR i hi
  rw [← Nat.cast_pow, ← hc, CharP.cast_eq_zero]
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ i = n
[PROOFSTEP]
apply hR i hi
[GOAL]
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n✝ : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : Fintype.card R = p ^ n
hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n
c : ℕ
hc✝ : CharP R c
hcpn : c ∣ p ^ n
i : ℕ
hi : i ≤ n
hc : c = p ^ i
⊢ ↑p ^ i = 0
[PROOFSTEP]
rw [← Nat.cast_pow, ← hc, CharP.cast_eq_zero]
[GOAL]
case intro.intro.intro
R✝ : Type u_1
inst✝³ : NonAssocRing R✝
inst✝² : Fintype R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
c : ℕ
hc✝ : CharP R c
i : ℕ
hc : c = p ^ i
hn : Fintype.card R = p ^ i
hR : ∀ (i_1 : ℕ), i_1 ≤ i → ↑p ^ i_1 = 0 → i_1 = i
hcpn : c ∣ p ^ i
hi : i ≤ i
⊢ CharP R (p ^ i)
[PROOFSTEP]
rwa [← hc]
[GOAL]
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S q
⊢ ∀ (x : ℕ), ↑x = 0 ↔ lcm p q ∣ x
[PROOFSTEP]
simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]
[GOAL]
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ CharP (R × S) p
[PROOFSTEP]
convert Nat.lcm.charP R S p p
[GOAL]
case h.e'_3
R : Type u_1
S : Type v
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ p = Nat.lcm p p
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ Set.InjOn Int.cast {0, 1, -1}
[PROOFSTEP]
rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h
[GOAL]
case inl.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑0
⊢ 0 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inl.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑1
⊢ 0 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑(-1)
⊢ 0 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑0
⊢ 1 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑1
⊢ 1 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑(-1)
⊢ 1 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑0
⊢ -1 = 0
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑1
⊢ -1 = 1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inr.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑(-1)
⊢ -1 = -1
[PROOFSTEP]
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
[GOAL]
case inr.inl.inr.inr
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ False
[PROOFSTEP]
exact (Ring.neg_one_ne_one_of_char_ne_two hR).symm h
[GOAL]
case inr.inr.inr.inl
R✝ : Type u_1
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ False
[PROOFSTEP]
exact (Ring.neg_one_ne_one_of_char_ne_two hR) h
[GOAL]
R : Type u_1
inst✝¹ : AddMonoidWithOne R
r : R
n p✝ : ℕ
a : ℕ+
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ¬p ∣ k
[PROOFSTEP]
rwa [← CharP.cast_eq_zero_iff R p k, ← Ne.def, ← neZero_iff]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
[PROOFSTEP]
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0
[PROOFSTEP]
simp [hp.ne_zero]
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R
[PROOFSTEP]
let p := ringChar R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R
[PROOFSTEP]
cases CharP.char_is_prime_or_zero R p with
| inl hp => simpa using h p hp
| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
x✝ : Nat.Prime p ∨ p = 0
⊢ CharZero R
[PROOFSTEP]
cases CharP.char_is_prime_or_zero R p with
| inl hp => simpa using h p hp
| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R
[PROOFSTEP]

| inl hp => simpa using h p hp
[GOAL]
case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R
[PROOFSTEP]
simpa using h p hp
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R
[PROOFSTEP]

| inr h =>
  haveI : CharP R 0 := h ▸ inferInstance
  exact CharP.charP_to_charZero R
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R
[PROOFSTEP]
haveI : CharP R 0 := h ▸ inferInstance
[GOAL]
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R
[PROOFSTEP]
exact CharP.charP_to_charZero R
