Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
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.6Semiring Ξ±: 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 + 1geom_sum_succ {x: Ξ±x : Ξ±: Type uΞ±} {n: βn : β: Typeβ} :
(β i: ?m.83i in range: β β Finset βrange (n: βn + 1: ?m.291), x: Ξ±x ^ i: ?m.83i) = (x: Ξ±x * β i: ?m.503i in range: β β Finset βrange n: βn, x: Ξ±x ^ i: ?m.503i) + 1: ?m.5951 := byGoals accomplished! π
Ξ±: Type uinstβ: 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 xmul_sum, β pow_succ: β {M : Type ?u.1137} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_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 0sum_range_succ', pow_zero: β {M : Type ?u.1180} [inst : Monoid M] (a : M), a ^ 0 = 1pow_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 + 1geom_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 ^ igeom_sum_succ' {x: Ξ±x : Ξ±: Type uΞ±} {n: βn : β: Typeβ} :
(β i: ?m.2123i in range: β β Finset βrange (n: βn + 1: ?m.20691), x: Ξ±x ^ i: ?m.2123i) = x: Ξ±x ^ n: βn + β i: ?m.2543i in range: β β Finset βrange n: βn, x: Ξ±x ^ i: ?m.2543i :=
(sum_range_succ: β {Ξ² : Type ?u.2943} [inst : AddCommMonoid Ξ²] (f : β β Ξ²) (n : β), β x in range (n + 1), f x = β x in range n, f x + f nsum_range_succ _: β β ?m.2944_ _: β_).trans: β {Ξ± : Sort ?u.2975} {a b c : Ξ±}, a = b β b = c β a = ctrans (add_comm: β {G : Type ?u.3002} [inst : AddCommSemigroup G] (a b : G), a + b = b + aadd_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 ^ igeom_sum_succ'

theorem geom_sum_zero: β (x : Ξ±), β i in range 0, x ^ i = 0geom_sum_zero (x: Ξ±x : Ξ±: Type uΞ±) : (β i: ?m.3281i in range: β β Finset βrange 0: ?m.32690, x: Ξ±x ^ i: ?m.3281i) = 0: ?m.36810 :=
rfl: β {Ξ± : Sort ?u.3846} {a : Ξ±}, a = arfl
#align geom_sum_zero geom_sum_zero: β {Ξ± : Type u} [inst : Semiring Ξ±] (x : Ξ±), β i in range 0, x ^ i = 0geom_sum_zero

theorem geom_sum_one: β (x : Ξ±), β i in range 1, x ^ i = 1geom_sum_one (x: Ξ±x : Ξ±: Type uΞ±) : (β i: ?m.3927i in range: β β Finset βrange 1: ?m.39151, x: Ξ±x ^ i: ?m.3927i) = 1: ?m.43271 := byGoals accomplished! π Ξ±: Type uinstβ: 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 ^ igeom_sum_succ']Goals accomplished! π
#align geom_sum_one geom_sum_one: β {Ξ± : Type u} [inst : Semiring Ξ±] (x : Ξ±), β i in range 1, x ^ i = 1geom_sum_one

@[simp]
theorem geom_sum_two: β {Ξ± : Type u} [inst : Semiring Ξ±] {x : Ξ±}, β i in range 2, x ^ i = x + 1geom_sum_two {x: Ξ±x : Ξ±: Type uΞ±} : (β i: ?m.4655i in range: β β Finset βrange 2: ?m.46442, x: Ξ±x ^ i: ?m.4655i) = x: Ξ±x + 1: ?m.50581 := byGoals accomplished! π Ξ±: Type uinstβ: 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 ^ igeom_sum_succ']Goals accomplished! π
#align geom_sum_two geom_sum_two: β {Ξ± : Type u} [inst : Semiring Ξ±] {x : Ξ±}, β i in range 2, x ^ i = x + 1geom_sum_two

@[simp]
theorem zero_geom_sum: β {Ξ± : Type u} [inst : Semiring Ξ±] {n : β}, β i in range n, 0 ^ i = if n = 0 then 0 else 1zero_geom_sum : β {n: ?m.5712n}, (β i: ?m.5724i in range: β β Finset βrange n: ?m.5712n, (0: ?m.57310 : Ξ±: Type uΞ±) ^ i: ?m.5724i) = if n: ?m.5712n = 0: ?m.62760 then 0: ?m.63050 else 1: ?m.63161
| 0: β0 => byGoals accomplished! π Ξ±: Type uinstβ: Semiring Ξ±β i in range 0, 0 ^ i = if 0 = 0 then 0 else 1simpGoals accomplished! π
| 1: β1 => byGoals accomplished! π Ξ±: Type uinstβ: Semiring Ξ±β i in range 1, 0 ^ i = if 1 = 0 then 0 else 1simpGoals accomplished! π
| n: βn + 2 => byGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±n: ββ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1rw [Ξ±: Type uinstβ: 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 ^ igeom_sum_succ'Ξ±: Type uinstβ: Semiring Ξ±n: β0 ^ (n + 1) + β i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1]Ξ±: Type uinstβ: Semiring Ξ±n: β0 ^ (n + 1) + β i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
Ξ±: Type uinstβ: 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 1zero_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 1zero_geom_sum

theorem one_geom_sum: β {Ξ± : Type u} [inst : Semiring Ξ±] (n : β), β i in range n, 1 ^ i = βnone_geom_sum (n: βn : β: Typeβ) : (β i: ?m.8490i in range: β β Finset βrange n: βn, (1: ?m.84971 : Ξ±: Type uΞ±) ^ i: ?m.8490i) = n: βn := byGoals accomplished! π Ξ±: Type uinstβ: Semiring Ξ±n: ββ i in range n, 1 ^ i = βnsimpGoals accomplished! π
#align one_geom_sum one_geom_sum: β {Ξ± : Type u} [inst : Semiring Ξ±] (n : β), β i in range n, 1 ^ i = βnone_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 ^ iop_geom_sum (x: Ξ±x : Ξ±: Type uΞ±) (n: βn : β: Typeβ) : op: {Ξ± : Type ?u.9667} β Ξ± β Ξ±α΅α΅α΅op (β i: ?m.9704i in range: β β Finset βrange n: βn, x: Ξ±x ^ i: ?m.9704i) = β i: ?m.10110i in range: β β Finset βrange n: βn, op: {Ξ± : Type ?u.10115} β Ξ± β Ξ±α΅α΅α΅op x: Ξ±x ^ i: ?m.10110i := byGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x: Ξ±n: βop (β i in range n, x ^ i) = β i in range n, op x ^ isimpGoals 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 ^ iop_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.10767i in range: β β Finset βrange n: βn, op: {Ξ± : Type ?u.10775} β Ξ± β Ξ±α΅α΅α΅op y: Ξ±y ^ (n: βn - 1: ?m.107841 - i: ?m.10767i) * op: {Ξ± : Type ?u.10797} β Ξ± β Ξ±α΅α΅α΅op x: Ξ±x ^ i: ?m.10767i =
β i: ?m.11707i in range: β β Finset βrange n: βn, op: {Ξ± : Type ?u.11715} β Ξ± β Ξ±α΅α΅α΅op y: Ξ±y ^ i: ?m.11707i * op: {Ξ± : Type ?u.11720} β Ξ± β Ξ±α΅α΅α΅op x: Ξ±x ^ (n: βn - 1: ?m.117291 - i: ?m.11707i):= byGoals accomplished! π
Ξ±: Type uinstβ: 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 xop_mul, op_pow: β {M : Type ?u.12229} [inst : Monoid M] (x : M) (n : β), op (x ^ n) = op x ^ nop_pow]Ξ±: Type uinstβ: 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 uinstβ: 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 uinstβ: 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 jsum_range_reflectΞ±: Type uinstβ: 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 uinstβ: 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 uinstβ: 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β gsum_congr rfl: β {Ξ± : Sort ?u.12606} {a : Ξ±}, a = arfl fun j: ?m.12610j j_in: ?m.12613j_in => _: ?m.12567 j = ?m.12568 j_Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j β range nop y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
Ξ±: Type uinstβ: 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 uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j β range nop 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 < nmem_range,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j < nop y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j) Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j β range nop 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 β€ nNat.lt_iff_add_one_leΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j + 1 β€ nop y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)]Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j + 1 β€ nop y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j) at j_in: ?m.12613j_inΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j + 1 β€ nop y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
Ξ±: Type uinstβ: 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 uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j + 1 β€ ne_a.e_an - 1 - (n - 1 - j) = j
Ξ±: Type uinstβ: 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) = atsub_tsub_cancel_of_leΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±n, j: βj_in: j + 1 β€ ne_a.e_a.hj β€ n - 1
Ξ±: Type uinstβ: 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 - ble_tsub_of_add_le_right j_in: j + 1 β€ nj_inGoals 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 ^ igeom_sumβ_with_one (x: Ξ±x : Ξ±: Type uΞ±) (n: βn : β: Typeβ) :
(β i: ?m.13877i in range: β β Finset βrange n: βn, x: Ξ±x ^ i: ?m.13877i * 1: ?m.138891 ^ (n: βn - 1: ?m.139061 - i: ?m.13877i)) = β i: ?m.14504i in range: β β Finset βrange n: βn, x: Ξ±x ^ i: ?m.14504i :=
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β gsum_congr rfl: β {Ξ± : Sort ?u.15315} {a : Ξ±}, a = arfl fun i: ?m.15322i _: ?m.15325_ => byGoals accomplished! π Ξ±: Type uinstβ: Semiring Ξ±x: Ξ±n, i: βxβ: i β range nx ^ i * 1 ^ (n - 1 - i) = x ^ irw [Ξ±: Type uinstβ: Semiring Ξ±x: Ξ±n, i: βxβ: i β range nx ^ i * 1 ^ (n - 1 - i) = x ^ ione_pow: β {M : Type ?u.15334} [inst : Monoid M] (n : β), 1 ^ n = 1one_pow,Ξ±: Type uinstβ: Semiring Ξ±x: Ξ±n, i: βxβ: i β range nx ^ i * 1 = x ^ i Ξ±: Type uinstβ: Semiring Ξ±x: Ξ±n, i: βxβ: i β range nx ^ i * 1 ^ (n - 1 - i) = x ^ imul_one: β {M : Type ?u.15433} [inst : MulOneClass M] (a : M), a * 1 = amul_oneΞ±: Type uinstβ: Semiring Ξ±x: Ξ±n, i: βxβ: i β range nx ^ 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 ^ igeom_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) ^ nCommute.geom_sumβ_mul_add {x: Ξ±x y: Ξ±y : Ξ±: Type uΞ±} (h: Commute x yh : Commute: {S : Type ?u.15532} β [inst : Mul S] β S β S β PropCommute x: Ξ±x y: Ξ±y) (n: βn : β: Typeβ) :
(β i: ?m.15717i in range: β β Finset βrange n: βn, (x: Ξ±x + y: Ξ±y) ^ i: ?m.15717i * y: Ξ±y ^ (n: βn - 1: ?m.157381 - i: ?m.15717i)) * x: Ξ±x + y: Ξ±y ^ n: βn = (x: Ξ±x + y: Ξ±y) ^ n: βn := byGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β 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.173121 - i: βi)Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β 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.178471 - i: βi) := Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β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) ^ nbyGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β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 β€ age_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 + btsub_le_iff_right, forall_const: β {b : Prop} (Ξ± : Sort ?u.18421) [i : Nonempty Ξ±], Ξ± β b β bforall_const]Goals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ nchange (β i: ?m.18689i in range: β β Finset βrange n: βn, (f: β β β β Ξ±f n: βn) i: ?m.18689i) * x: Ξ±x + y: Ξ±y ^ n: βn = (x: Ξ±x + y: Ξ±y) ^ n: βnΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β 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 nihΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ nΒ·Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 = 0sum_empty,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 = 0zero_mul,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 = azero_add,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 = 1pow_zero,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 = 1pow_zeroΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yn: β(β i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ nΒ·Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β 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) ^ nf_last : f: β β β β Ξ±f (n: βn + 1: ?m.203061) n: βn = (x: Ξ±x + y: Ξ±y) ^ n: βn := Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nbyGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ nrw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ nhf: β (m i : β), f m i = (x + y) ^ i * y ^ (m - 1 - i)hf,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (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 - ctsub_add_eq_tsub_tsub,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ nNat.add_comm: β (n m : β), n + m = m + nNat.add_comm,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ ntsub_self: β {Ξ± : Type ?u.20886} [inst : CanonicallyOrderedAddMonoid Ξ±] [inst_1 : Sub Ξ±] [inst_2 : OrderedSub Ξ±] (a : Ξ±), a - a = 0tsub_self,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ npow_zero: β {M : Type ?u.20971} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf (n + 1) n = (x + y) ^ nmul_one: β {M : Type ?u.21036} [inst : MulOneClass M] (a : M), a * 1 = amul_oneΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β 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 if_succ : β i: ?m.21112i, i: ?m.21112i β range: β β Finset βrange n: βn β f: β β β β Ξ±f (n: βn + 1: ?m.211511) i: ?m.21112i = y: Ξ±y * f: β β β β Ξ±f n: βn i: ?m.21112i := fun i: ?m.21309i hi: ?m.21312hi => Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nbyGoals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n irw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n ihf: β (m i : β), f m i = (x + y) ^ i * y ^ (m - 1 - i)hfΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range n(x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i]Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range n(x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n ihave : Commute: {S : Type ?u.21345} β [inst : Mul S] β S β S β PropCommute y: Ξ±y ((x: Ξ±x + y: Ξ±y) ^ i: βi) := (h: Commute x yh.symm: β {S : Type ?u.21676} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm.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 aCommute.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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n irw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = y * (x + y) ^ i * y ^ (n - 1 - i) Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 * aeq,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y * y ^ (n - 1 - i) Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * (y * y ^ (n - 1 - i)) Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 ^ npow_succ y: Ξ±y (n: βn - 1: ?m.220561 - i: βi)Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y ^ (n - 1 - i + 1)]Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)(x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y ^ (n - 1 - i + 1)
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n icongr 2Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)e_a.e_an + 1 - 1 - i = n - 1 - i + 1
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n irw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 = aadd_tsub_cancel_right,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)e_a.e_an - i = n - 1 - i + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 - ctsub_add_eq_tsub_tsub,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)e_a.e_an - i = n - (1 + i) + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: 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 + aadd_comm 1: ?m.229241 i: βiΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)e_a.e_an - i = n - (i + 1) + 1]Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthis: Commute y ((x + y) ^ i)e_a.e_an - i = n - (i + 1) + 1
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n ihave : i: βi + 1: ?m.229591 + (n: βn - (i: βi + 1: ?m.229761)) = 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) = badd_tsub_cancel_of_le (mem_range: β {n m : β}, m β range n β m < nmem_range.mp: β {a b : Prop}, (a β b) β a β bmp hi: i β range nhi)Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: i + 1 + (n - (i + 1)) = ne_a.e_an - i = n - (i + 1) + 1
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n irw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: i + 1 + (n - (i + 1)) = ne_a.e_an - i = n - (i + 1) + 1add_comm: β {G : Type ?u.23397} [inst : AddCommSemigroup G] (a b : G), a + b = b + aadd_comm (i: βi + 1: ?m.234041)Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - i = n - (i + 1) + 1]Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - i = n - (i + 1) + 1 at this: i + 1 + (n - (i + 1)) = nthisΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - i = n - (i + 1) + 1
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nf (n + 1) i = y * f n irw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - i = n - (i + 1) + 1β this: n - (i + 1) + (i + 1) = nthis,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - (i + 1) + (i + 1) - i = n - (i + 1) + (i + 1) - (i + 1) + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_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 = aadd_tsub_cancel_right,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - (i + 1) + (i + 1) - i = n - (i + 1) + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - i = n - (i + 1) + 1add_comm: β {G : Type ?u.23691} [inst : AddCommSemigroup G] (a b : G), a + b = b + aadd_comm i: βi 1: ?m.236951,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - (1 + i) + (1 + i) - i = n - (1 + i) + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - (1 + i) + 1 + i - i = n - (1 + i) + 1 Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_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 = aadd_tsub_cancel_rightΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ ni: βhi: i β range nthisβ: Commute y ((x + y) ^ i)this: n - (i + 1) + (i + 1) = ne_a.e_an - (1 + i) + 1 = n - (1 + i) + 1]Goals accomplished! π
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 ^ npow_succ (x: Ξ±x + y: Ξ±y),Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) * (x + y) ^ n Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 * cadd_mul,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 xsum_range_succ_comm,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 * cadd_mul,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isuccf (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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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) ^ nf_last,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(β 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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 aCommute.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 yh).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 * aeqΞ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc(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 uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ ncongr 1Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc.e_a(β x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nsucc(β i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ nrw [Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc.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β gsum_congr rfl: β {Ξ± : Sort ?u.25871} {a : Ξ±}, a = arfl f_succ: β (i : β), i β range n β f (n + 1) i = y * f n if_succ,Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= 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) ^ nf_last: f (n + 1) n = (x + y) ^ nf_succ: β (i : β), i β range n β f (n + 1) i = y * f n isucc.e_a(β x in range n, y * f n x) * x + y ^ Nat.succ n = y * (x + y) ^ n Ξ±: Type uinstβ: Semiring Ξ±x, y: Ξ±h: Commute x yf:= fun m i => (x + y) ^ i * y ^ (m - 1 - i): β β β β Ξ±hf: β (m i : β), f