case zero
R : Type u
S : Type v
A : Type w
B : Type ?u.557702
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.zero = (x - ↑(algebraMap R A) r) ^ Nat.zero * x

case succ
R : Type u
S : Type v
A : Type w
B : Type ?u.557702
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.succ n = (x - ↑(algebraMap R A) r) ^ Nat.succ n * x
R : Type u
S : Type v
A : Type w
B : Type ?u.557702
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
⊢ x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
induction' n with n ih
no goals
case zero
R : Type u
S : Type v
A : Type w
B : Type ?u.557702
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.zero = (x - ↑(algebraMap R A) r) ^ Nat.zero * x
simp
no goals
case succ
R : Type u
S : Type v
A : Type w
B : Type ?u.557702
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.succ n = (x - ↑(algebraMap R A) r) ^ Nat.succ n * x
rw [pow_succ, ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]