case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
⊢ ↑1 = 1

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑1 = 1
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
⊢ ↑1 = 1
cases' n with n
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑(1 % (n + 1)) = 1
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑1 = 1
show ((1 % (n + 1) : ℕ) : R) = 1
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.succ Nat.zero
⊢ ↑(1 % (Nat.zero + 1)) = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑(1 % (Nat.succ n✝ + 1)) = 1
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ Nat.succ n
⊢ ↑(1 % (n + 1)) = 1
cases n
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑1 = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ 1 < Nat.succ n✝ + 1
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑(1 % (Nat.succ n✝ + 1)) = 1
rw [Nat.mod_eq_of_lt]
no goals
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ 1 < Nat.succ n✝ + 1
exact Nat.lt_of_sub_eq_succ rfl
no goals
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
⊢ ↑1 = 1
exact Int.cast_one
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.succ Nat.zero
⊢ ↑(1 % (Nat.zero + 1)) = 1
rw [Nat.dvd_one] at h
case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
subst m
no goals
case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (Nat.zero + 1)) = 1
apply Subsingleton.elim
no goals
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ (Nat.succ n✝)
⊢ ↑1 = 1
exact Nat.cast_one