case inl
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ ↑(k - 1) = ↑n - 1

case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
⊢ ↑(k - 1) = (if k = 0 then ↑n else ↑k) - 1
split_ifs with hk
no goals
case inl
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ ↑(k - 1) = ↑n - 1
rw [hk, zero_sub, ZMod.cast_neg_one]
case inr.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1

case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
cases n
case inr.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
case inr.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
dsimp [ZMod, ZMod.cast]
no goals
case inr.zero
R : Type u_1
inst✝ : Ring R
k : ZMod Nat.zero
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
rw [Int.cast_sub, Int.cast_one]
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1
dsimp [ZMod, ZMod.cast, ZMod.val]
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

case inr.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ¬k = 0
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑↑(k - 1) = ↑↑k - 1
rw [Fin.coe_sub_one, if_neg]
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ 1 ≤ ↑k
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1
rw [Nat.cast_sub, Nat.cast_one]
no goals
case inr.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ 1 ≤ ↑k
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
no goals
case inr.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (Nat.succ n✝)
hk : ¬k = 0
⊢ ¬k = 0
exact hk