R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i (↑C r * X ^ n))
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (↑C r * X ^ n) i
refine' ⟨r * a ^ n * b ^ (N - n), bi, bu, _⟩
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * (↑i r * eval (↑i a * bi) X ^ n)
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * eval (↑i a * bi) (Polynomial.map i (↑C r * X ^ n))
rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n) * (↑i r * ↑i a ^ n) = ↑i b ^ N * (↑i r * (↑i a * bi) ^ n)
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i (r * a ^ n * b ^ (N - n)) = ↑i b ^ N * (↑i r * eval (↑i a * bi) X ^ n)
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, eval_X, mul_comm]
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n) * (↑i r * ↑i a ^ n) = ↑i b ^ N * (↑i r * (↑i a * bi) ^ n)
rw [← tsub_add_cancel_of_le nN]
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * (↑i a * (bi * ↑i b)) ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * ↑i a ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
conv_lhs => rw [← mul_one (i a), ← bu]
no goals
R : Type u_2
K : Type u_1
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a✝ b : R
bi : K
N : ℕ
a : R
bu : bi * ↑i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ ↑i b ^ (N - n + n - n) * (↑i r * (↑i a * (bi * ↑i b)) ^ n) = ↑i b ^ (N - n + n) * (↑i r * (↑i a * bi) ^ n)
simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]