case zero
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i in range Nat.zero, x ^ i * y ^ (Nat.zero - 1 - i) = ∑ i in range Nat.zero, y ^ i * x ^ (Nat.zero - 1 - i)

case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i in range (Nat.succ n✝), x ^ i * y ^ (Nat.succ n✝ - 1 - i) =
    ∑ i in range (Nat.succ n✝), y ^ i * x ^ (Nat.succ n✝ - 1 - i)
α✝ α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
h : Commute x y
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = ∑ i in range n, y ^ i * x ^ (n - 1 - i)
cases n
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 in range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i in range (Nat.succ n✝), x ^ i * y ^ (Nat.succ n✝ - 1 - i) =
    ∑ i in range (Nat.succ n✝), y ^ i * x ^ (Nat.succ n✝ - 1 - i)
simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r in range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 in range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
rw [← Finset.sum_flip]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r in range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
refine' Finset.sum_congr rfl fun i hi => _
no goals
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _
no goals
case zero
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i in range Nat.zero, x ^ i * y ^ (Nat.zero - 1 - i) = ∑ i in range Nat.zero, y ^ i * x ^ (Nat.zero - 1 - i)
simp