α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
let f :  ℕ → ℕ → α := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
have hf : ∀ m i : ℕ, f m i = (x + y) ^ i * y ^ (m - 1 - i) := by
  simp only [ge_iff_le, tsub_le_iff_right, forall_const]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
change (∑ i in range n, (f n) i) * x + y ^ n = (x + y) ^ n
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zero

case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
induction' n with n ih
no goals
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
simp only [ge_iff_le, tsub_le_iff_right, forall_const]
no goals
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zero
rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
have f_last : f (n + 1) n = (x + y) ^ n := by
  rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
  rw [hf]
  have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
  rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
  congr 2
  rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
  have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
  rw [add_comm (i + 1)] at this
  rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = x * (x + y) ^ n + y * (x + y) ^ n
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = (x + y) ^ n * x + y * (x + y) ^ n
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = x * (x + y) ^ n + y * (x + y) ^ n
rw [(((Commute.refl x).add_right h).pow_right n).eq]
case succ.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = (x + y) ^ n * x + y * (x + y) ^ n
congr 1
no goals
case succ.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
rw [sum_congr rfl f_succ, ← mul_sum, pow_succ y, mul_assoc, ← mul_add y, ih]
no goals
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ f (n + 1) n = (x + y) ^ n
rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ f (n + 1) i = y * f n i
rw [hf]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y ^ (n - 1 - i + 1)
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n + 1 - 1 - i = n - 1 - i + 1
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y ^ (n - 1 - i + 1)
congr 2
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n - i = n - (i + 1) + 1
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n + 1 - 1 - i = n - 1 - i + 1
rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ n - i = n - (i + 1) + 1
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n - i = n - (i + 1) + 1
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ n - i = n - (i + 1) + 1
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ n - i = n - (i + 1) + 1
rw [add_comm (i + 1)] at this
no goals
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ n - i = n - (i + 1) + 1
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]