/-
Copyright (c) 2019 Neil Strickland. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Neil Strickland

! This file was ported from Lean 3 source module algebra.geom_sum
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Tactic.Abel
import Mathlib.Data.Nat.Parity

/-!
# Partial sums of geometric series

This file determines the values of the geometric series $\sum_{i=0}^{n-1} x^i$ and
$\sum_{i=0}^{n-1} x^i y^{n-1-i}$ and variants thereof. We also provide some bounds on the
"geometric" sum of `a/b^i` where `a b : ℕ`.

## Main statements

* `geom_sum_Ico` proves that $\sum_{i=m}^{n-1} x^i=\frac{x^n-x^m}{x-1}$ in a division ring.
* `geom_sum₂_Ico` proves that $\sum_{i=m}^{n-1} x^iy^{n - 1 - i}=\frac{x^n-y^{n-m}x^m}{x-y}$
  in a field.

Several variants are recorded, generalising in particular to the case of a noncommutative ring in
which `x` and `y` commute. Even versions not using division or subtraction, valid in each semiring,
are recorded.
-/

--porting note: corrected type in the description of `geom_sum₂_Ico` (in the doc string only).

universe u

variable {α: Type u
α : Type u: Type (u+1)
Type u}

open Finset MulOpposite

open BigOperators

section Semiring

variable [Semiring: Type ?u.6 → Type ?u.6
Semiring α: Type u
α]

theorem geom_sum_succ: ∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x * ∑ i in range n, x ^ i + 1
geom_sum_succ {x: α
x : α: Type u
α} {n: ℕ
n : ℕ: Type
ℕ} :
    (∑ i: ?m.83
i in range: ℕ → Finset ℕ
range (n: ℕ
n + 1: ?m.29
1), x: α
x ^ i: ?m.83
i) = (x: α
x * ∑ i: ?m.503
i in range: ℕ → Finset ℕ
range n: ℕ
n, x: α
x ^ i: ?m.503
i) + 1: ?m.595
1 := by
Goals accomplished! 🐙
  α: Type u

inst✝: Semiring α

x: α

n: ℕ

∑ i in range (n + 1), x ^ i = x * ∑ i in range n, x ^ i + 1simp only [mul_sum: ∀ {α : Type ?u.1111} {β : Type ?u.1110} {s : Finset α} {b : β} {f : α → β} [inst : NonUnitalNonAssocSemiring β],
  b * ∑ x in s, f x = ∑ x in s, b * f x
mul_sum, ← pow_succ: ∀ {M : Type ?u.1137} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ, sum_range_succ': ∀ {β : Type ?u.1163} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ),
  ∑ k in range (n + 1), f k = ∑ k in range n, f (k + 1) + f 0
sum_range_succ', pow_zero: ∀ {M : Type ?u.1180} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero]
Goals accomplished! 🐙
#align geom_sum_succ geom_sum_succ: ∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x * ∑ i in range n, x ^ i + 1
geom_sum_succ

theorem geom_sum_succ': ∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x ^ n + ∑ i in range n, x ^ i
geom_sum_succ' {x: α
x : α: Type u
α} {n: ℕ
n : ℕ: Type
ℕ} :
    (∑ i: ?m.2123
i in range: ℕ → Finset ℕ
range (n: ℕ
n + 1: ?m.2069
1), x: α
x ^ i: ?m.2123
i) = x: α
x ^ n: ℕ
n + ∑ i: ?m.2543
i in range: ℕ → Finset ℕ
range n: ℕ
n, x: α
x ^ i: ?m.2543
i :=
  (sum_range_succ: ∀ {β : Type ?u.2943} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ), ∑ x in range (n + 1), f x = ∑ x in range n, f x + f n
sum_range_succ _: ℕ → ?m.2944
_ _: ℕ
_).trans: ∀ {α : Sort ?u.2975} {a b c : α}, a = b → b = c → a = c
trans (add_comm: ∀ {G : Type ?u.3002} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm _: ?m.3003
_ _: ?m.3003
_)
#align geom_sum_succ' geom_sum_succ': ∀ {α : Type u} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x ^ n + ∑ i in range n, x ^ i
geom_sum_succ'

theorem geom_sum_zero: ∀ (x : α), ∑ i in range 0, x ^ i = 0
geom_sum_zero (x: α
x : α: Type u
α) : (∑ i: ?m.3281
i in range: ℕ → Finset ℕ
range 0: ?m.3269
0, x: α
x ^ i: ?m.3281
i) = 0: ?m.3681
0 :=
  rfl: ∀ {α : Sort ?u.3846} {a : α}, a = a
rfl
#align geom_sum_zero geom_sum_zero: ∀ {α : Type u} [inst : Semiring α] (x : α), ∑ i in range 0, x ^ i = 0
geom_sum_zero

theorem geom_sum_one: ∀ (x : α), ∑ i in range 1, x ^ i = 1
geom_sum_one (x: α
x : α: Type u
α) : (∑ i: ?m.3927
i in range: ℕ → Finset ℕ
range 1: ?m.3915
1, x: α
x ^ i: ?m.3927
i) = 1: ?m.4327
1 := by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

x: α

∑ i in range 1, x ^ i = 1simp [geom_sum_succ': ∀ {α : Type ?u.4380} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x ^ n + ∑ i in range n, x ^ i
geom_sum_succ']
Goals accomplished! 🐙
#align geom_sum_one geom_sum_one: ∀ {α : Type u} [inst : Semiring α] (x : α), ∑ i in range 1, x ^ i = 1
geom_sum_one

@[simp]
theorem geom_sum_two: ∀ {α : Type u} [inst : Semiring α] {x : α}, ∑ i in range 2, x ^ i = x + 1
geom_sum_two {x: α
x : α: Type u
α} : (∑ i: ?m.4655
i in range: ℕ → Finset ℕ
range 2: ?m.4644
2, x: α
x ^ i: ?m.4655
i) = x: α
x + 1: ?m.5058
1 := by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

x: α

∑ i in range 2, x ^ i = x + 1simp [geom_sum_succ': ∀ {α : Type ?u.5332} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x ^ n + ∑ i in range n, x ^ i
geom_sum_succ']
Goals accomplished! 🐙
#align geom_sum_two geom_sum_two: ∀ {α : Type u} [inst : Semiring α] {x : α}, ∑ i in range 2, x ^ i = x + 1
geom_sum_two

@[simp]
theorem zero_geom_sum: ∀ {α : Type u} [inst : Semiring α] {n : ℕ}, ∑ i in range n, 0 ^ i = if n = 0 then 0 else 1
zero_geom_sum : ∀ {n: ?m.5712
n}, (∑ i: ?m.5724
i in range: ℕ → Finset ℕ
range n: ?m.5712
n, (0: ?m.5731
0 : α: Type u
α) ^ i: ?m.5724
i) = if n: ?m.5712
n = 0: ?m.6276
0 then 0: ?m.6305
0 else 1: ?m.6316
1
  | 0: ℕ
0 => by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

∑ i in range 0, 0 ^ i = if 0 = 0 then 0 else 1simp
Goals accomplished! 🐙
  | 1: ℕ
1 => by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

∑ i in range 1, 0 ^ i = if 1 = 0 then 0 else 1simp
Goals accomplished! 🐙
  | n: ℕ
n + 2 => by
Goals accomplished! 🐙
    α: Type u

inst✝: Semiring α

n: ℕ

∑ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1rw [α: Type u

inst✝: Semiring α

n: ℕ

∑ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1geom_sum_succ': ∀ {α : Type ?u.7465} [inst : Semiring α] {x : α} {n : ℕ}, ∑ i in range (n + 1), x ^ i = x ^ n + ∑ i in range n, x ^ i
geom_sum_succ'α: Type u

inst✝: Semiring α

n: ℕ

0 ^ (n + 1) + ∑ i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1]α: Type u

inst✝: Semiring α

n: ℕ

0 ^ (n + 1) + ∑ i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
    α: Type u

inst✝: Semiring α

n: ℕ

∑ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1simp [zero_geom_sum: ∀ {n : ℕ}, ∑ i in range n, 0 ^ i = if n = 0 then 0 else 1
zero_geom_sum]
Goals accomplished! 🐙
#align zero_geom_sum zero_geom_sum: ∀ {α : Type u} [inst : Semiring α] {n : ℕ}, ∑ i in range n, 0 ^ i = if n = 0 then 0 else 1
zero_geom_sum

theorem one_geom_sum: ∀ {α : Type u} [inst : Semiring α] (n : ℕ), ∑ i in range n, 1 ^ i = ↑n
one_geom_sum (n: ℕ
n : ℕ: Type
ℕ) : (∑ i: ?m.8490
i in range: ℕ → Finset ℕ
range n: ℕ
n, (1: ?m.8497
1 : α: Type u
α) ^ i: ?m.8490
i) = n: ℕ
n := by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

n: ℕ

∑ i in range n, 1 ^ i = ↑nsimp
Goals accomplished! 🐙
#align one_geom_sum one_geom_sum: ∀ {α : Type u} [inst : Semiring α] (n : ℕ), ∑ i in range n, 1 ^ i = ↑n
one_geom_sum

-- porting note: simp can prove this
-- @[simp]
theorem op_geom_sum: ∀ (x : α) (n : ℕ), op (∑ i in range n, x ^ i) = ∑ i in range n, op x ^ i
op_geom_sum (x: α
x : α: Type u
α) (n: ℕ
n : ℕ: Type
ℕ) : op: {α : Type ?u.9667} → α → αᵐᵒᵖ
op (∑ i: ?m.9704
i in range: ℕ → Finset ℕ
range n: ℕ
n, x: α
x ^ i: ?m.9704
i) = ∑ i: ?m.10110
i in range: ℕ → Finset ℕ
range n: ℕ
n, op: {α : Type ?u.10115} → α → αᵐᵒᵖ
op x: α
x ^ i: ?m.10110
i := by
Goals accomplished! 🐙
  α: Type u

inst✝: Semiring α

x: α

n: ℕ

op (∑ i in range n, x ^ i) = ∑ i in range n, op x ^ isimp
Goals accomplished! 🐙
#align op_geom_sum op_geom_sum: ∀ {α : Type u} [inst : Semiring α] (x : α) (n : ℕ), op (∑ i in range n, x ^ i) = ∑ i in range n, op x ^ i
op_geom_sum

--porting note: linter suggested to change left hand side
@[simp]
theorem op_geom_sum₂: ∀ {α : 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)
op_geom_sum₂ (x: α
x y: α
y : α: Type u
α) (n: ℕ
n : ℕ: Type
ℕ) : ∑ i: ?m.10767
i in range: ℕ → Finset ℕ
range n: ℕ
n, op: {α : Type ?u.10775} → α → αᵐᵒᵖ
op y: α
y ^ (n: ℕ
n - 1: ?m.10784
1 - i: ?m.10767
i) * op: {α : Type ?u.10797} → α → αᵐᵒᵖ
op x: α
x ^ i: ?m.10767
i =
    ∑ i: ?m.11707
i in range: ℕ → Finset ℕ
range n: ℕ
n, op: {α : Type ?u.11715} → α → αᵐᵒᵖ
op y: α
y ^ i: ?m.11707
i * op: {α : Type ?u.11720} → α → αᵐᵒᵖ
op x: α
x ^ (n: ℕ
n - 1: ?m.11729
1 - i: ?m.11707
i):= by
Goals accomplished! 🐙
  α: 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: ∀ {β : Type ?u.12191} {α : Type ?u.12190} [inst : AddCommMonoid β] {s : Finset α} (f : α → β),
  op (∑ x in s, f x) = ∑ x in s, op (f x)
op_sum, op_mul: ∀ {α : Type ?u.12211} [inst : Mul α] (x y : α), op (x * y) = op y * op x
op_mul, op_pow: ∀ {M : Type ?u.12229} [inst : Monoid M] (x : M) (n : ℕ), op (x ^ n) = op x ^ n
op_pow]α: 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)rw [α: 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)← sum_range_reflect: ∀ {δ : Type ?u.12477} [inst : AddCommMonoid δ] (f : ℕ → δ) (n : ℕ), ∑ j in range n, f (n - 1 - j) = ∑ j in range n, f j
sum_range_reflectα: 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: ℕ

∑ 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)refine' sum_congr: ∀ {β : Type ?u.12562} {α : Type ?u.12561} {s₁ s₂ : Finset α} {f g : α → β} [inst : AddCommMonoid β],
  s₁ = s₂ → (∀ (x : α), x ∈ s₂ → f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g
sum_congr rfl: ∀ {α : Sort ?u.12606} {a : α}, a = a
rfl fun j: ?m.12610
j j_in: ?m.12613
j_in => _: ?m.12567 j = ?m.12568 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)
  α: 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 [α: 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)mem_range: ∀ {n m : ℕ}, m ∈ range n ↔ m < n
mem_range,α: Type u

inst✝: Semiring α

x, y: α

n, j: ℕ

j_in: j < 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)Nat.lt_iff_add_one_le: ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n
Nat.lt_iff_add_one_leα: 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 + 1 ≤ n

op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j) at j_in: ?m.12613
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: ℕ

∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)congrα: Type u

inst✝: Semiring α

x, y: α

n, j: ℕ

j_in: j + 1 ≤ n

e_a.e_an - 1 - (n - 1 - j) = j
  α: 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)apply tsub_tsub_cancel_of_le: ∀ {α : Type ?u.13190} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
  [inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
  {a b : α} [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → b - (b - a) = a
tsub_tsub_cancel_of_leα: Type u

inst✝: Semiring α

x, y: α

n, j: ℕ

j_in: j + 1 ≤ n

e_a.e_a.hj ≤ n - 1
  α: 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)exact le_tsub_of_add_le_right: ∀ {α : Type ?u.13611} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  {a b c : α} [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b ≤ c → a ≤ c - b
le_tsub_of_add_le_right j_in: j + 1 ≤ n
j_in
Goals accomplished! 🐙
#align op_geom_sum₂ op_geom_sum₂: ∀ {α : 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)
op_geom_sum₂

theorem geom_sum₂_with_one: ∀ (x : α) (n : ℕ), ∑ i in range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i in range n, x ^ i
geom_sum₂_with_one (x: α
x : α: Type u
α) (n: ℕ
n : ℕ: Type
ℕ) :
    (∑ i: ?m.13877
i in range: ℕ → Finset ℕ
range n: ℕ
n, x: α
x ^ i: ?m.13877
i * 1: ?m.13889
1 ^ (n: ℕ
n - 1: ?m.13906
1 - i: ?m.13877
i)) = ∑ i: ?m.14504
i in range: ℕ → Finset ℕ
range n: ℕ
n, x: α
x ^ i: ?m.14504
i :=
  sum_congr: ∀ {β : Type ?u.15267} {α : Type ?u.15266} {s₁ s₂ : Finset α} {f g : α → β} [inst : AddCommMonoid β],
  s₁ = s₂ → (∀ (x : α), x ∈ s₂ → f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g
sum_congr rfl: ∀ {α : Sort ?u.15315} {a : α}, a = a
rfl fun i: ?m.15322
i _: ?m.15325
_ => by
Goals accomplished! 🐙 α: Type u

inst✝: Semiring α

x: α

n, i: ℕ

x✝: i ∈ range n

x ^ i * 1 ^ (n - 1 - i) = x ^ irw [α: Type u

inst✝: Semiring α

x: α

n, i: ℕ

x✝: i ∈ range n

x ^ i * 1 ^ (n - 1 - i) = x ^ ione_pow: ∀ {M : Type ?u.15334} [inst : Monoid M] (n : ℕ), 1 ^ n = 1
one_pow,α: Type u

inst✝: Semiring α

x: α

n, i: ℕ

x✝: i ∈ range n

x ^ i * 1 = x ^ i α: Type u

inst✝: Semiring α

x: α

n, i: ℕ

x✝: i ∈ range n

x ^ i * 1 ^ (n - 1 - i) = x ^ imul_one: ∀ {M : Type ?u.15433} [inst : MulOneClass M] (a : M), a * 1 = a
mul_oneα: Type u

inst✝: Semiring α

x: α

n, i: ℕ

x✝: i ∈ range n

x ^ i = x ^ i]
Goals accomplished! 🐙
#align geom_sum₂_with_one geom_sum₂_with_one: ∀ {α : Type u} [inst : Semiring α] (x : α) (n : ℕ), ∑ i in range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i in range n, x ^ i
geom_sum₂_with_one

/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
protected theorem Commute.geom_sum₂_mul_add: ∀ {α : Type u} [inst : Semiring α] {x y : α},
  Commute x y → ∀ (n : ℕ), (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
Commute.geom_sum₂_mul_add {x: α
x y: α
y : α: Type u
α} (h: Commute x y
h : Commute: {S : Type ?u.15532} → [inst : Mul S] → S → S → Prop
Commute x: α
x y: α
y) (n: ℕ
n : ℕ: Type
ℕ) :
    (∑ i: ?m.15717
i in range: ℕ → Finset ℕ
range n: ℕ
n, (x: α
x + y: α
y) ^ i: ?m.15717
i * y: α
y ^ (n: ℕ
n - 1: ?m.15738
1 - i: ?m.15717
i)) * x: α
x + y: α
y ^ n: ℕ
n = (x: α
x + y: α
y) ^ n: ℕ
n := by
Goals accomplished! 🐙
  α: 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) ^ nlet f: ℕ → ℕ → α
f :  ℕ: Type
ℕ → ℕ: Type
ℕ → α: Type u
α := fun m: ℕ
m i: ℕ
i : ℕ: Type
ℕ => (x: α
x + y: α
y) ^ i: ℕ
i * y: α
y ^ (m: ℕ
m - 1: ?m.17312
1 - i: ℕ
i)α: 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
  -- porting note: adding `hf` here, because below in two places `dsimp [f]` didn't work
  α: 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) ^ nhave hf: ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ m: ℕ
m i: ℕ
i : ℕ: Type
ℕ, f: ℕ → ℕ → α
f m: ℕ
m i: ℕ
i = (x: α
x + y: α
y) ^ i: ℕ
i * y: α
y ^ (m: ℕ
m - 1: ?m.17847
1 - i: ℕ
i) := α: 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) ^ nby
Goals accomplished! 🐙
    α: 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: ∀ {α : Type ?u.18361} [inst : LE α] {a b : α}, a ≥ b ↔ b ≤ a
ge_iff_le, tsub_le_iff_right: ∀ {α : Type ?u.18381} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
  a - b ≤ c ↔ a ≤ c + b
tsub_le_iff_right, forall_const: ∀ {b : Prop} (α : Sort ?u.18421) [i : Nonempty α], α → b ↔ b
forall_const]
Goals accomplished! 🐙
  α: 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) ^ nchange (∑ i: ?m.18689
i in range: ℕ → Finset ℕ
range n: ℕ
n, (f: ℕ → ℕ → α
f n: ℕ
n) i: ?m.18689
i) * x: α
x + y: α
y ^ n: ℕ
n = (x: α
x + y: α
y) ^ n: ℕ
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
  α: 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) ^ ninduction' n: ℕ
n with n: ℕ
n ih: ?m.19775 n
ihα: 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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.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)

n: ℕ

ih: (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n

succ(∑ 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: ℕ

(∑ 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

f:= fun m i => (x + y) ^ i * y ^ (m - 1 - i): ℕ → ℕ → α

hf: ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.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)

n: ℕ

ih: (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [α: 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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zerorange_zero: range 0 = ∅
range_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)

zero(∑ i in ∅, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zerosum_empty: ∀ {β : Type ?u.19793} {α : Type ?u.19792} {f : α → β} [inst : AddCommMonoid β], ∑ x in ∅, f x = 0
sum_empty,α: 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)

zero0 * x + y ^ Nat.zero = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zerozero_mul: ∀ {M₀ : Type ?u.19865} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul,α: 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)

zero0 + y ^ Nat.zero = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zerozero_add: ∀ {M : Type ?u.20012} [inst : AddZeroClass M] (a : M), 0 + a = a
zero_add,α: 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)

zeroy ^ Nat.zero = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zeropow_zero: ∀ {M : Type ?u.20165} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_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)

zero1 = (x + y) ^ Nat.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)

zero(∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zeropow_zero: ∀ {M : Type ?u.20243} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_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)

zero1 = 1]
Goals accomplished! 🐙
  α: 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·α: 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

succ(∑ 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

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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nhave f_last: f (n + 1) n = (x + y) ^ n
f_last : f: ℕ → ℕ → α
f (n: ℕ
n + 1: ?m.20306
1) n: ℕ
n = (x: α
x + y: α
y) ^ n: ℕ
n := α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nby
Goals accomplished! 🐙
      α: 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) ^ nrw [α: 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) ^ nhf: ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
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

(x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n α: 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← tsub_add_eq_tsub_tsub: ∀ {α : Type ?u.20580} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub,α: 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

(x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n α: 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) ^ nNat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm,α: 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

(x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n α: 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) ^ ntsub_self: ∀ {α : Type ?u.20886} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] (a : α), a - a = 0
tsub_self,α: 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

(x + y) ^ n * y ^ 0 = (x + y) ^ n α: 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) ^ npow_zero: ∀ {M : Type ?u.20971} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_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)

n: ℕ

ih: (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n

(x + y) ^ n * 1 = (x + y) ^ n α: 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) ^ nmul_one: ∀ {M : Type ?u.21036} [inst : MulOneClass M] (a : M), a * 1 = a
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

(x + y) ^ n = (x + y) ^ n]
Goals accomplished! 🐙
    α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nhave f_succ: ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
f_succ : ∀ i: ?m.21112
i, i: ?m.21112
i ∈ range: ℕ → Finset ℕ
range n: ℕ
n → f: ℕ → ℕ → α
f (n: ℕ
n + 1: ?m.21151
1) i: ?m.21112
i = y: α
y * f: ℕ → ℕ → α
f n: ℕ
n i: ?m.21112
i := fun i: ?m.21309
i hi: ?m.21312
hi => α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nby
Goals accomplished! 🐙
      α: 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 irw [α: 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 ihf: ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
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

(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
      α: 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 ihave : Commute: {S : Type ?u.21345} → [inst : Mul S] → S → S → Prop
Commute y: α
y ((x: α
x + y: α
y) ^ i: ℕ
i) := (h: Commute x y
h.symm: ∀ {S : Type ?u.21676} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm.add_right: ∀ {R : Type ?u.21685} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)
add_right (Commute.refl: ∀ {S : Type ?u.21788} [inst : Mul S] (a : S), Commute a a
Commute.refl y: α
y)).pow_right: ∀ {M : Type ?u.21791} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right i: ℕ
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) = 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 irw [α: 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← mul_assoc: ∀ {G : Type ?u.21808} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,α: 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 * (x + y) ^ i * y ^ (n - 1 - 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) = y * f n ithis: Commute y ((x + y) ^ i)
this.eq: ∀ {S : Type ?u.21976} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq,α: 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 * y ^ (n - 1 - 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) = y * f n imul_assoc: ∀ {G : Type ?u.21989} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc,α: 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 * y ^ (n - 1 - 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) = y * f n i← pow_succ: ∀ {M : Type ?u.22046} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ y: α
y (n: ℕ
n - 1: ?m.22056
1 - i: ℕ
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) = (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

f (n + 1) i = y * f n icongr 2α: 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)

e_a.e_an + 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

f (n + 1) i = y * f n irw [α: 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)

e_a.e_an + 1 - 1 - i = n - 1 - i + 1add_tsub_cancel_right: ∀ {α : Type ?u.22406} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
add_tsub_cancel_right,α: 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)

e_a.e_an - 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)

e_a.e_an + 1 - 1 - i = n - 1 - i + 1← tsub_add_eq_tsub_tsub: ∀ {α : Type ?u.22738} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
  (a b c : α), a - (b + c) = a - b - c
tsub_add_eq_tsub_tsub,α: 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)

e_a.e_an - 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)

e_a.e_an + 1 - 1 - i = n - 1 - i + 1add_comm: ∀ {G : Type ?u.22920} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm 1: ?m.22924
1 i: ℕ
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)

e_a.e_an - i = n - (i + 1) + 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)

e_a.e_an - i = n - (i + 1) + 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

f (n + 1) i = y * f n ihave : i: ℕ
i + 1: ?m.22959
1 + (n: ℕ
n - (i: ℕ
i + 1: ?m.22976
1)) = n: ℕ
n := add_tsub_cancel_of_le: ∀ {α : Type ?u.23092} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
  [inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
  {a b : α}, a ≤ b → a + (b - a) = b
add_tsub_cancel_of_le (mem_range: ∀ {n m : ℕ}, m ∈ range n ↔ m < n
mem_range.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hi: i ∈ range n
hi)α: 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

e_a.e_an - i = n - (i + 1) + 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

f (n + 1) i = y * f n irw [α: 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

e_a.e_an - i = n - (i + 1) + 1add_comm: ∀ {G : Type ?u.23397} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm (i: ℕ
i + 1: ?m.23404
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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 1 at this: i + 1 + (n - (i + 1)) = n
thisα: 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

e_a.e_an - i = n - (i + 1) + 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

f (n + 1) i = y * f n irw [α: 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

e_a.e_an - i = n - (i + 1) + 1← this: n - (i + 1) + (i + 1) = n
this,α: 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

e_a.e_an - (i + 1) + (i + 1) - i = n - (i + 1) + (i + 1) - (i + 1) + 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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 1add_tsub_cancel_right: ∀ {α : Type ?u.23472} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
add_tsub_cancel_right,α: 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

e_a.e_an - (i + 1) + (i + 1) - i = n - (i + 1) + 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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 1add_comm: ∀ {G : Type ?u.23691} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm i: ℕ
i 1: ?m.23695
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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - (1 + i) + (1 + i) - 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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 1← add_assoc: ∀ {G : Type ?u.23700} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assoc,α: 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

e_a.e_an - (1 + i) + 1 + i - 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)

this: n - (i + 1) + (i + 1) = n

e_a.e_an - i = n - (i + 1) + 1add_tsub_cancel_right: ∀ {α : Type ?u.23757} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
add_tsub_cancel_rightα: 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

e_a.e_an - (1 + i) + 1 = n - (1 + i) + 1]
Goals accomplished! 🐙
    α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ npow_succ: ∀ {M : Type ?u.23969} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ (x: α
x + y: α
y),α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) * (x + y) ^ n α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nadd_mul: ∀ {R : Type ?u.24094} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
  (a + b) * c = a * c + b * c
add_mul,α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = x * (x + y) ^ n + y * (x + y) ^ n α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nsum_range_succ_comm: ∀ {β : Type ?u.24402} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ),
  ∑ x in range (n + 1), f x = f n + ∑ x in range n, f x
sum_range_succ_comm,α: 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

succ(f (Nat.succ n) n + ∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = x * (x + y) ^ n + y * (x + y) ^ n α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nadd_mul: ∀ {R : Type ?u.24468} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
  (a + b) * c = a * c + b * c
add_mul,α: 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

succf (Nat.succ n) n * x + (∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = x * (x + y) ^ n + y * (x + y) ^ n α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nf_last: f (n + 1) n = (x + y) ^ n
f_last,α: 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

succ(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 α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nadd_assoc: ∀ {G : Type ?u.24662} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
add_assocα: 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

succ(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]α: 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

succ(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
    α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [α: 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

succ(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(((Commute.refl: ∀ {S : Type ?u.24827} [inst : Mul S] (a : S), Commute a a
Commute.refl x: α
x).add_right: ∀ {R : Type ?u.24830} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)
add_right h: Commute x y
h).pow_right: ∀ {M : Type ?u.24843} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
pow_right n: ℕ
n).eq: ∀ {S : Type ?u.24856} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eqα: 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

succ(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]α: 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

succ(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
    α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ ncongr 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

f_succ: ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i

succ.e_a(∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
    α: 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

succ(∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [α: 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

succ.e_a(∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ nsum_congr: ∀ {β : Type ?u.25863} {α : Type ?u.25862} {s₁ s₂ : Finset α} {f g : α → β} [inst : AddCommMonoid β],
  s₁ = s₂ → (∀ (x : α), x ∈ s₂ → f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g
sum_congr rfl: ∀ {α : Sort ?u.25871} {a : α}, a = a
rfl f_succ: ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
f_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

succ.e_a(∑ x in range n, y * f n x) * x + y ^ Nat.succ n = y * (x + y) ^ n α: 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