α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
simp only [op_sum, op_mul, op_pow]
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ j in range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
rw [← sum_range_reflect]
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ j in range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
refine' sum_congr rfl fun j j_in => _
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
rw [mem_range, Nat.lt_iff_add_one_le] at j_in
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
congr
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j
apply tsub_tsub_cancel_of_le
no goals
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1
exact le_tsub_of_add_le_right j_in