case h.zero
R : Type u_1
S : Type ?u.96790
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(coeff R Nat.zero) (invUnitsSub u * X) = ↑(coeff R Nat.zero) (invUnitsSub u * ↑(C R) ↑u - 1)

case h.succ
R : Type u_1
S : Type ?u.96790
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
n : ℕ
⊢ ↑(coeff R (Nat.succ n)) (invUnitsSub u * X) = ↑(coeff R (Nat.succ n)) (invUnitsSub u * ↑(C R) ↑u - 1)
R : Type u_1
S : Type ?u.96790
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ invUnitsSub u * X = invUnitsSub u * ↑(C R) ↑u - 1
ext (_ | n)
no goals
case h.zero
R : Type u_1
S : Type ?u.96790
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(coeff R Nat.zero) (invUnitsSub u * X) = ↑(coeff R Nat.zero) (invUnitsSub u * ↑(C R) ↑u - 1)
simp
no goals
case h.succ
R : Type u_1
S : Type ?u.96790
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
n : ℕ
⊢ ↑(coeff R (Nat.succ n)) (invUnitsSub u * X) = ↑(coeff R (Nat.succ n)) (invUnitsSub u * ↑(C R) ↑u - 1)
simp [n.succ_ne_zero, pow_succ]