[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ : ℕ
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (?m.60081 x✝ p k hp hk hn + 1) = n
[PROOFSTEP]
rwa [Nat.sub_add_cancel hk]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n p : R
k : ℕ
inst✝ : NoZeroDivisors R
⊢ ¬IsPrimePow 0
[PROOFSTEP]
simp only [isPrimePow_def, not_exists, not_and', and_imp]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n p : R
k : ℕ
inst✝ : NoZeroDivisors R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
[PROOFSTEP]
intro x n _hn hx
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n✝ p : R
k : ℕ
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x
[PROOFSTEP]
rw [pow_eq_zero hx]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n✝ p : R
k : ℕ
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k : ℕ
p : R
hp : Prime p
⊢ p ^ 1 = p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ : ℕ
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k
[PROOFSTEP]
rw [pow_mul', hn]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
simp only [isPrimePow_def, Nat.prime_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, _⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃ p_1, p_1 ≤ p ^ k ∧ ∃ k_1, k_1 ≤ p ^ k ∧ Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k
[PROOFSTEP]
refine' ⟨p, _, k, (Nat.lt_pow_self hp.one_lt _).le, hp, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k
[PROOFSTEP]
conv => {lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
{lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
{lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
lhs
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p
[PROOFSTEP]
rw [← (pow_one p)]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ 1 ≤ p ^ k
[PROOFSTEP]
exact (Nat.pow_le_iff_le_right hp.two_le).mpr hk
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m
[PROOFSTEP]
rw [isPrimePow_nat_iff] at hn ⊢
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
[PROOFSTEP]
rcases hn with ⟨p, k, hp, _hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
[PROOFSTEP]
obtain ⟨i, hik, rfl⟩ := (Nat.dvd_prime_pow hp).1 hm
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
[PROOFSTEP]
refine' ⟨p, i, hp, _, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case intro.intro.intro.intro.intro.intro.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False
[PROOFSTEP]
simp only [pow_zero, ne_eq] at hm₁
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))
[PROOFSTEP]
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
[PROOFSTEP]
rintro n han _ha hn hbn _hb -
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False
[PROOFSTEP]
exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)


[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
⊢ Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
[PROOFSTEP]
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r b c
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r b c
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
[PROOFSTEP]
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (fun x x_1 => x * x_1) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
⊢ Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
[PROOFSTEP]
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
⊢ r b c
[PROOFSTEP]
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
[GOAL]
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Covariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r b c
⊢ r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
[PROOFSTEP]
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
[GOAL]
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝¹ : CovariantClass M N μ r
inst✝ : Group N
h : Contravariant N N (swap fun x x_1 => x * x_1) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
[PROOFSTEP]
exact h a⁻¹ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
[PROOFSTEP]
intro h a b c bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b c : N
bc : b ≤ c
⊢ μ a b ≤ μ a c
[PROOFSTEP]
rcases le_iff_eq_or_lt.mp bc with (rfl | bc)
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b
[PROOFSTEP]
exact rfl.le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Covariant M N μ fun x x_1 => x < x_1
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c
[PROOFSTEP]
exact (h _ bc).le
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
[PROOFSTEP]
refine fun h a b c bc ↦ lt_iff_le_and_ne.mpr ⟨h a bc.le, ?_⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Contravariant M N μ fun x x_1 => x ≤ x_1
a : M
b c : N
bc : (fun x x_1 => x < x_1) (μ a b) (μ a c)
⊢ b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : PartialOrder N
h : Contravariant M N μ fun x x_1 => x ≤ x_1
a : M
b : N
bc : μ a b < μ a b
⊢ False
[PROOFSTEP]
exact lt_irrefl _ bc
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : CommSemigroup N
⊢ Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
[PROOFSTEP]
rw [flip_mul]
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝ : CommSemigroup N
⊢ Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
[PROOFSTEP]
rw [flip_mul]
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc : b < c
⊢ a * b < a * c
[PROOFSTEP]
cases' lt_iff_le_and_ne.mp bc with bc cb
[GOAL]
case intro
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc✝ : b < c
bc : b ≤ c
cb : b ≠ c
⊢ a * b < a * c
[PROOFSTEP]
exact lt_iff_le_and_ne.mpr ⟨CovariantClass.elim a bc, (mul_ne_mul_right a).mpr cb⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc : b < c
⊢ swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
cases' lt_iff_le_and_ne.mp bc with bc cb
[GOAL]
case intro
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : N
bc✝ : b < c
bc : b ≤ c
cb : b ≠ c
⊢ swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
[PROOFSTEP]
exact lt_iff_le_and_ne.mpr ⟨CovariantClass.elim a bc, (mul_ne_mul_left a).mpr cb⟩
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
⊢ b ≤ c
[PROOFSTEP]
cases' le_iff_eq_or_lt.mp bc with h h
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
h : a * b = a * c
⊢ b ≤ c
[PROOFSTEP]
exact ((mul_right_inj a).mp h).le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : LeftCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : a * b ≤ a * c
h : a * b < a * c
⊢ b ≤ c
[PROOFSTEP]
exact (ContravariantClass.elim _ h).le
[GOAL]
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
cases' le_iff_eq_or_lt.mp bc with h h
[GOAL]
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
h : swap (fun x x_1 => x * x_1) a b = swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
exact ((mul_left_inj a).mp h).le
[GOAL]
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst✝² : RightCancelSemigroup N
inst✝¹ : PartialOrder N
inst✝ : ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : N
bc : swap (fun x x_1 => x * x_1) a b ≤ swap (fun x x_1 => x * x_1) a c
h : swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
⊢ b ≤ c
[PROOFSTEP]
exact (ContravariantClass.elim _ h).le


[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ ∑ i in range (n + 1), x ^ i = x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
simp only [mul_sum, ← pow_succ, sum_range_succ', pow_zero]
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i in range 1, x ^ i = 1
[PROOFSTEP]
simp [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i in range 2, x ^ i = x + 1
[PROOFSTEP]
simp [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
⊢ ∑ i in range 0, 0 ^ i = if 0 = 0 then 0 else 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
⊢ ∑ i in range 1, 0 ^ i = if 1 = 0 then 0 else 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1
[PROOFSTEP]
rw [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ 0 ^ (n + 1) + ∑ i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
[PROOFSTEP]
simp [zero_geom_sum]
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i in range n, 1 ^ i = ↑n
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ op (∑ i in range n, x ^ i) = ∑ i in range n, op x ^ i
[PROOFSTEP]
simp
[GOAL]
α : 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)
[PROOFSTEP]
rw [← sum_range_reflect]
[GOAL]
α : 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)
[PROOFSTEP]
refine' sum_congr rfl fun j j_in => _
[GOAL]
α : 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)
[PROOFSTEP]
rw [mem_range, Nat.lt_iff_add_one_le] at j_in
[GOAL]
α : 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)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j
[PROOFSTEP]
apply tsub_tsub_cancel_of_le
[GOAL]
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1
[PROOFSTEP]
exact le_tsub_of_add_le_right j_in
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 ^ (n - 1 - i) = x ^ i
[PROOFSTEP]
rw [one_pow, mul_one]
[GOAL]
α : 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
[PROOFSTEP]
let f : ℕ → ℕ → α := fun m i : ℕ =>
  (x + y) ^ i *
    y ^
      (m - 1 - i)
        -- porting note: adding `hf` here, because below in two places `dsimp [f]` didn't work
[GOAL]
α : 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
[PROOFSTEP]
have hf : ∀ m i : ℕ, f m i = (x + y) ^ i * y ^ (m - 1 - i) := by simp only [ge_iff_le, tsub_le_iff_right, forall_const]
[GOAL]
α : 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)
[PROOFSTEP]
simp only [ge_iff_le, tsub_le_iff_right, forall_const]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
[PROOFSTEP]
change (∑ i in range n, (f n) i) * x + y ^ n = (x + y) ^ n
[GOAL]
α : 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
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zero
[PROOFSTEP]
rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
have f_last : f (n + 1) n = (x + y) ^ n := by
  rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
[GOAL]
α : 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
[PROOFSTEP]
rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi =>
  by
  rw [hf]
  have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
  rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
  congr 2
  rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
  have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
  rw [add_comm (i + 1)] at this
  rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ f (n + 1) i = y * f n i
[PROOFSTEP]
rw [hf]
[GOAL]
α : 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
[PROOFSTEP]
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
[GOAL]
α : 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
[PROOFSTEP]
rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
[GOAL]
α : 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)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n + 1 - 1 - i = n - 1 - i + 1
[PROOFSTEP]
rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
rw [add_comm (i + 1)] at this
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = x * (x + y) ^ n + y * (x + y) ^ n
[PROOFSTEP]
rw [(((Commute.refl x).add_right h).pow_right n).eq]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = (x + y) ^ n * x + y * (x + y) ^ n
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
[PROOFSTEP]
rw [sum_congr rfl f_succ, ← mul_sum, pow_succ y, mul_assoc, ← mul_add y, ih]
[GOAL]
α : Type u
inst✝ : Ring α
n : ℕ
⊢ ∑ i in range n, (-1) ^ i = if Even n then 0 else 1
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
α : Type u
inst✝ : Ring α
⊢ ∑ i in range Nat.zero, (-1) ^ i = if Even Nat.zero then 0 else 1
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i in range (Nat.succ k), (-1) ^ i = if Even (Nat.succ k) then 0 else 1
[PROOFSTEP]
simp only [geom_sum_succ', Nat.even_add_one, hk]
[GOAL]
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1
[PROOFSTEP]
rw [h.neg_one_pow, add_zero]
[GOAL]
case neg
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
[PROOFSTEP]
rw [(Nat.odd_iff_not_even.2 h).neg_one_pow, neg_add_self]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ ∑ i in range n, x ^ i * x ^ (n - 1 - i) = ∑ i in range n, x ^ (i + (n - 1 - i))
[PROOFSTEP]
simp_rw [← pow_add]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ card (range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)
[PROOFSTEP]
rw [Finset.card_range, nsmul_eq_mul]
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
have := (Commute.one_right x).geom_sum₂_mul_add n
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
rw [one_pow, geom_sum₂_with_one] at this
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
rw [sub_add_cancel] at this
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
rw [← this, add_sub_cancel]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
[PROOFSTEP]
apply op_injective
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
[PROOFSTEP]
simp only [op_mul, op_sub, op_geom_sum₂, op_pow]
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n
[PROOFSTEP]
simp [(Commute.op h.symm).geom_sum₂_mul n]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (x - y) * ∑ i in range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
[PROOFSTEP]
rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
[GOAL]
α : Type u
x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
cases' le_or_lt y x with h h
[GOAL]
case inl
α : Type u
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
[GOAL]
case inl
α : Type u
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
[GOAL]
case inr
α : Type u
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
[GOAL]
case inr
α : Type u
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
have h₁ := geom_sum₂_mul x (-y) n
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
exact Dvd.intro_left _ h₁
[GOAL]
α : Type u
x y n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
exact_mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
have := (Commute.one_right x).geom_sum₂_mul n
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
rw [one_pow, geom_sum₂_with_one] at this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((x - 1) * ∑ i in range n, x ^ i) = op (x ^ n - 1)
[PROOFSTEP]
simpa using geom_sum_mul (op x) n
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
have := congr_arg Neg.neg (geom_sum_mul x n)
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : -((∑ i in range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
rw [neg_sub, ← mul_neg, neg_sub] at this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((1 - x) * ∑ i in range n, x ^ i) = op (1 - x ^ n)
[PROOFSTEP]
simpa using geom_sum_mul_neg (op x) n
[GOAL]
α✝ α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
h : Commute x y
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = ∑ i in range n, y ^ i * x ^ (n - 1 - i)
[PROOFSTEP]
cases n
[GOAL]
case zero
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i in range Nat.zero, x ^ i * y ^ (Nat.zero - 1 - i) = ∑ i in range Nat.zero, y ^ i * x ^ (Nat.zero - 1 - i)
[PROOFSTEP]
simp
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i in range (Nat.succ n✝), x ^ i * y ^ (Nat.succ n✝ - 1 - i) =
    ∑ i in range (Nat.succ n✝), y ^ i * x ^ (Nat.succ n✝ - 1 - i)
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 in range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
[PROOFSTEP]
rw [← Finset.sum_flip]
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r in range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
[PROOFSTEP]
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
[PROOFSTEP]
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
[PROOFSTEP]
rw [← h'.geom_sum₂_mul, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
[PROOFSTEP]
have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
[PROOFSTEP]
rw [← geom_sum_mul, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
have : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) :=
  by
  refine' sum_congr rfl fun j j_in => _
  rw [← pow_add]
  congr
  rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in
  have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
  rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
[PROOFSTEP]
refine' sum_congr rfl fun j j_in => _
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))
[PROOFSTEP]
rw [← pow_add]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
h' : n - m + (m - (1 + j)) = n - (1 + j)
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
simp_rw [pow_mul_comm y (n - m) _]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
simp_rw [← mul_assoc]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add, add_tsub_cancel_of_le hmn,
  sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i in range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i in range n, x ^ i * y ^ (n - 1 - i)
[PROOFSTEP]
simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
  (h.symm.pow_right _).eq, mul_assoc, ← pow_succ]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i in range n, x ^ i * y ^ (n - i) = ∑ x_1 in range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1)
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
[PROOFSTEP]
suffices n - 1 - i + 1 = n - i by rw [this]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
[PROOFSTEP]
rw [this]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ n - 1 - i + 1 = n - i
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
i : ℕ
hi : i ∈ range Nat.zero
⊢ Nat.zero - 1 - i + 1 = Nat.zero - i
[PROOFSTEP]
exact absurd (List.mem_range.mp hi) i.not_lt_zero
[GOAL]
case succ
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
i n : ℕ
hi : i ∈ range (Nat.succ n)
⊢ Nat.succ n - 1 - i + 1 = Nat.succ n - i
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (Nat.le_pred_of_lt (List.mem_range.mp hi)),
  tsub_add_cancel_of_le (Nat.succ_le_iff.mpr n.succ_pos)]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
[PROOFSTEP]
apply op_injective
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ MulOpposite.op ((∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
[PROOFSTEP]
simp only [op_sub, op_mul, op_pow, op_sum]
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
have :
  (∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) :=
  by
  refine' sum_congr rfl fun k _ => _
  have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
  simpa [Commute, SemiconjBy] using hp
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
refine' sum_congr rfl fun k _ => _
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
simpa [Commute, SemiconjBy] using hp
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
simp only [this]
  -- porting note: gives deterministic timeout without this intermediate `have`
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
convert (Commute.op h).mul_geom_sum₂_Ico hmn
[GOAL]
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
[GOAL]
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
[PROOFSTEP]
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
[PROOFSTEP]
rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
[PROOFSTEP]
simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
[PROOFSTEP]
simp only [geom_sum_Ico hx hmn]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ n - x ^ m) / (x - 1) = (x ^ m - x ^ n) / (1 - x)
[PROOFSTEP]
convert neg_div_neg_eq (x ^ m - x ^ n) (1 - x) using 2
[GOAL]
case h.e'_2.h.e'_5
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - x ^ m = -(x ^ m - x ^ n)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - x ^ m = -(x ^ m - x ^ n)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x - 1 = -(1 - x)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x - 1 = -(1 - x)
[PROOFSTEP]
abel
[GOAL]
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rcases le_or_lt m n with (hmn | hmn)
[GOAL]
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rw [geom_sum_Ico' h'x.ne hmn]
[GOAL]
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
[PROOFSTEP]
apply div_le_div (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
[GOAL]
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m
[PROOFSTEP]
simpa using pow_nonneg hx _
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rw [Ico_eq_empty, sum_empty]
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)
[PROOFSTEP]
apply div_nonneg (pow_nonneg hx _)
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ 1 - x
[PROOFSTEP]
simpa using h'x.le
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ¬m < n
[PROOFSTEP]
simpa using hmn.le
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne.def, div_eq_iff_mul_eq hx0, one_mul]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ x⁻¹ ≠ 1
[PROOFSTEP]
rwa [inv_eq_one_div, Ne.def, div_eq_iff_mul_eq hx0, one_mul]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₂ : x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
  Nat.recOn n (by simp) fun n h => by
    rw [pow_succ, mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc, inv_mul_cancel hx0]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ x * (x ^ Nat.zero)⁻¹ = (x ^ Nat.zero)⁻¹ * x
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x ^ Nat.succ n)⁻¹ = (x ^ Nat.succ n)⁻¹ * x
[PROOFSTEP]
rw [pow_succ, mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc, inv_mul_cancel hx0]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
[PROOFSTEP]
simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, add_left_comm]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
[PROOFSTEP]
rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x : α
n : ℕ
f : α →+* β
⊢ ↑f (∑ i in range n, x ^ i) = ∑ i in range n, ↑f x ^ i
[PROOFSTEP]
simp [f.map_sum]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x y : α
n : ℕ
f : α →+* β
⊢ ↑f (∑ i in range n, x ^ i * y ^ (n - 1 - i)) = ∑ i in range n, ↑f x ^ i * ↑f y ^ (n - 1 - i)
[PROOFSTEP]
simp [f.map_sum]
[GOAL]
α : Type u
β : Type u_1
a b n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i =
    ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
[PROOFSTEP]
rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero, Nat.div_one]
[GOAL]
α : Type u
β : Type u_1
a b n : ℕ
⊢ ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n) ≤
    ∑ i in range n, a / b ^ i + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
[PROOFSTEP]
refine' tsub_le_tsub_right (add_le_add_right (sum_le_sum fun i _ => _) _) _
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / (b ^ i * b) * b ≤ a / b ^ i
[PROOFSTEP]
rw [← Nat.div_div_eq_div_mul]
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
[PROOFSTEP]
exact Nat.div_mul_le_self _ _
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in range n, a / b ^ i ≤ a * b / (b - 1)
[PROOFSTEP]
refine' (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 _
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range n, a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i in range zero, a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
rw [sum_range_zero, zero_mul]
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range (succ n), a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i ≤ a * b
[PROOFSTEP]
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 n, a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i in Ico 1 zero, a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
rw [zero_eq, Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 (succ n), a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
rw [← add_le_add_iff_left a]
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i ≤ a + a / (b - 1)
[PROOFSTEP]
calc
  (a + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i := by
    rw [pow_zero, Nat.div_one]
  _ = ∑ i in range n.succ, a / b ^ i :=
    by
    rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
    exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
  _ ≤ a * b / (b - 1) := (Nat.geom_sum_le hb a _)
  _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
  _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i = a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i
[PROOFSTEP]
rw [pow_zero, Nat.div_one]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i = ∑ i in range (succ n), a / b ^ i
[PROOFSTEP]
rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ¬0 ∈ Ico (succ 0) (succ n)
[PROOFSTEP]
exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
[PROOFSTEP]
rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
[PROOFSTEP]
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedSemiring α
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
[PROOFSTEP]
refine' Nat.le_induction _ _ n (show 2 ≤ n from hn)
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i in range 2, x ^ i ∧ ∑ i in range 2, x ^ i < 1
[PROOFSTEP]
rw [geom_sum_two]
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < x + 1 ∧ x + 1 < 1
[PROOFSTEP]
exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 →
        0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
clear hn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 →
        0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
intro n _ ihn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hn✝ : 2 ≤ n
ihn : 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
⊢ 0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hn✝ : 2 ≤ n
ihn : 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
⊢ -x * ∑ i in range n, x ^ i < 1 ∧ x * ∑ i in range n, x ^ i < 0
[PROOFSTEP]
exact
  ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
    mul_neg_of_neg_of_pos hx ihn.1⟩
[GOAL]
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
⊢ if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
[PROOFSTEP]
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
[GOAL]
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
hx0 : x ≤ 0
⊢ if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even Nat.zero then ∑ i in range Nat.zero, x ^ i ≤ 0 else 1 ≤ ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, range_zero, sum_empty, le_refl, ite_true]
[GOAL]
case succ
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
⊢ if Even (Nat.succ n) then ∑ i in range (Nat.succ n), x ^ i ≤ 0 else 1 ≤ ∑ i in range (Nat.succ n), x ^ i
[PROOFSTEP]
simp only [Nat.even_add_one, geom_sum_succ]
[GOAL]
case succ
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
split_ifs at ih  with h
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i in range n, x ^ i ≤ 0
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg (not_not_intro h), le_add_iff_nonneg_left]
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i in range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i in range n, x ^ i
[PROOFSTEP]
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ x * ∑ i in range n, x ^ i + 1 ≤ 0
[PROOFSTEP]
refine' (add_le_add_right _ _).trans hx
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ x * ∑ i in range n, x ^ i ≤ x
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
⊢ if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
[PROOFSTEP]
have hx0 : x < 0 := ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
[PROOFSTEP]
refine' Nat.le_induction _ _ n (show 2 ≤ n from hn)
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i in range 2, x ^ i < 0 else 1 < ∑ i in range 2, x ^ i
[PROOFSTEP]
simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i) →
        if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
clear hn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i) →
        if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
intro n _ ihn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
⊢ if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
simp only [Nat.even_add_one, geom_sum_succ]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
by_cases hn' : Even n
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
hn' : Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos hn'] at ihn
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg, lt_add_iff_pos_left]
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ 0 < x * ∑ i in range n, x ^ i
case pos.hnc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ ¬¬Even n
[PROOFSTEP]
exact mul_pos_of_neg_of_neg hx0 ihn
[GOAL]
case pos.hnc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ ¬¬Even n
[PROOFSTEP]
exact not_not_intro hn'
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg hn'] at ihn
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos]
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i in range n, x ^ i + 1 < 0
case neg.hc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n
[PROOFSTEP]
swap
[GOAL]
case neg.hc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n
[PROOFSTEP]
exact hn'
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
have := add_lt_add_right (mul_lt_mul_of_neg_left ihn hx0) 1
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
this : x * ∑ i in range n, x ^ i + 1 < x * 1 + 1
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
rw [mul_one] at this
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
this : x * ∑ i in range n, x ^ i + 1 < x + 1
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
exact this.trans hx
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
obtain _ | _ | n := n
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.zero ≠ 0
⊢ 0 < ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
cases hn rfl
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.succ Nat.zero ≠ 0
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, zero_lt_one]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
obtain hx' | hx' := lt_or_le x 0
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : x < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1
[GOAL]
case succ.succ.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne.def, not_false_iff])
[GOAL]
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ Nat.succ (Nat.succ n) ≠ 0
[PROOFSTEP]
simp only [Nat.succ_ne_zero, Ne.def, not_false_iff]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
h : Odd n
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
rcases n with (_ | _ | k)
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ 0 < ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
exact ((show ¬Odd 0 by decide) h).elim
[GOAL]
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ ¬Odd 0
[PROOFSTEP]
decide
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd (Nat.succ Nat.zero)
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, geom_sum_one, zero_lt_one]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
rw [Nat.odd_iff_not_even] at h
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ k)) then ∑ i in range (Nat.succ (Nat.succ k)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
simp only [h, if_false] at this
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this : 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
exact zero_lt_one.trans this
[GOAL]
case succ.succ.inr.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 = 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]
[GOAL]
case succ.succ.inr.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : 0 < x + 1
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
exact geom_sum_pos' hx k.succ.succ_ne_zero
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i ↔ Odd n ∨ 0 < x + 1
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Odd n ∨ 0 < x + 1
[PROOFSTEP]
rw [or_iff_not_imp_left, ← not_le, ← Nat.even_iff_not_odd]
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
[PROOFSTEP]
refine' fun hn hx => h.not_le _
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i in range n, x ^ i ≤ 0
[PROOFSTEP]
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
rintro (hn | hx')
[GOAL]
case refine'_2.inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
exact hn.geom_sum_pos
[GOAL]
case refine'_2.inr
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
exact geom_sum_pos' hx' hn
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
obtain _ | _ | n := n
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.zero ≠ 0
⊢ ∑ i in range Nat.zero, x ^ i ≠ 0
[PROOFSTEP]
cases hn rfl
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.succ Nat.zero ≠ 0
⊢ ∑ i in range (Nat.succ Nat.zero), x ^ i ≠ 0
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_iff]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
rw [Ne.def, eq_neg_iff_add_eq_zero, ← Ne.def] at hx
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
obtain h | h := hx.lt_or_lt
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ n)) then ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
split_ifs at this
[GOAL]
case pos
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : Even (Nat.succ (Nat.succ n))
this : ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact this.ne
[GOAL]
case neg
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : ¬Even (Nat.succ (Nat.succ n))
this : 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact (zero_lt_one.trans this).ne'
[GOAL]
case succ.succ.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : 0 < x + 1
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i = 0 ↔ x = -1 ∧ Even n
[PROOFSTEP]
refine' ⟨fun h => _, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i in range n, x ^ i = 0
[PROOFSTEP]
simp only [h, hn, neg_one_geom_sum, if_true]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i in range n, x ^ i = 0
⊢ x = -1 ∧ Even n
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
have hx := eq_or_ne x (-1)
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
rw [hx, neg_one_geom_sum]
[GOAL]
case inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
[PROOFSTEP]
simp only [h hx, ne_eq, ite_eq_left_iff, one_ne_zero, not_forall, exists_prop, and_true]
[GOAL]
case inr
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
exact geom_sum_ne_zero hx hn
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0
[PROOFSTEP]
rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm, or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn),
  Nat.odd_iff_not_even, ← add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
  and_comm, Decidable.and_or_imp, or_comm]


[GOAL]
α : Type u_1
inst✝⁴ : Add α
inst✝³ : Mul α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = ↑sym (⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ ↑unsym (a * b) = ⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ ↑sym ⅟a * ↑sym a = 1
[PROOFSTEP]
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
[GOAL]
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ ↑sym a * ↑sym ⅟a = 1
[PROOFSTEP]
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑sym (⅟2 * (↑unsym a * (↑unsym b + ↑unsym c) + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a))) =
    ↑sym (⅟2 * (↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)))
[PROOFSTEP]
congr 2
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * (↑unsym b + ↑unsym c) + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym b + ↑unsym a * ↑unsym c + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
abel
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym b + ↑unsym a * ↑unsym c + (↑unsym b * ↑unsym a + ↑unsym c * ↑unsym a) =
    ↑unsym a * ↑unsym b + ↑unsym b * ↑unsym a + (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑sym (⅟2 * (↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + ↑unsym c * (↑unsym a + ↑unsym b))) =
    ↑sym (⅟2 * (↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)))
[PROOFSTEP]
congr 2
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + ↑unsym c * (↑unsym a + ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + (↑unsym c * ↑unsym a + ↑unsym c * ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
abel
[GOAL]
case h.e_6.h.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
a b c : αˢʸᵐ
⊢ ↑unsym a * ↑unsym c + ↑unsym b * ↑unsym c + (↑unsym c * ↑unsym a + ↑unsym c * ↑unsym b) =
    ↑unsym a * ↑unsym c + ↑unsym c * ↑unsym a + (↑unsym b * ↑unsym c + ↑unsym c * ↑unsym b)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ 0 * x✝ = 0
[PROOFSTEP]
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ x✝ * 0 = 0
[PROOFSTEP]
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ 1 * x✝ = x✝
[PROOFSTEP]
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
src✝ : AddCommMonoid αˢʸᵐ := addCommMonoid
x✝ : αˢʸᵐ
⊢ x✝ * 1 = x✝
[PROOFSTEP]
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_self_assoc, sym_unsym]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ ↑unsym (a * a) = ↑unsym a * ↑unsym a
[PROOFSTEP]
rw [mul_def, unsym_sym, ← two_mul, invOf_mul_self_assoc]
[GOAL]
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ ↑sym (a * a) = ↑sym a * ↑sym a
[PROOFSTEP]
rw [sym_mul_sym, ← two_mul, invOf_mul_self_assoc]
[GOAL]
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a
[PROOFSTEP]
rw [mul_def, mul_def, add_comm]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
have commute_half_left := fun a : α => by
  -- Porting note: mathlib3 used `bit0_left`
  have := (Commute.one_left a).add_left (Commute.one_left a)
  rw [one_add_one_eq_two] at this
  exact this.invOf_left.eq
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
⊢ ?m.76920 a
[PROOFSTEP]
have := (Commute.one_left a).add_left (Commute.one_left a)
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute (1 + 1) a
⊢ ?m.76920 a
[PROOFSTEP]
rw [one_add_one_eq_two] at this
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a✝ b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ ?m.76920 a
[PROOFSTEP]
exact this.invOf_left.eq
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ a * b * (a * a) = a * (b * (a * a))
[PROOFSTEP]
calc
  a * b * (a * a)
  _ =
      sym
        (⅟2 * ⅟2 *
          (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
            unsym (a * a) * unsym b * unsym a)) :=
    ?_
  _ =
      sym
        (⅟2 *
          (unsym a * unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
            unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) :=
    ?_
  _ = a * (b * (a * a)) :=
    ?_
      -- Rearrange LHS
[GOAL]
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ a * b * (a * a) =
    ↑sym
      (⅟2 * ⅟2 *
        (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
            ↑unsym (a * a) * ↑unsym a * ↑unsym b +
          ↑unsym (a * a) * ↑unsym b * ↑unsym a))
[PROOFSTEP]
rw [mul_def, mul_def a b, unsym_sym, ← mul_assoc, ← commute_half_left (unsym (a * a)), mul_assoc, mul_assoc, ← mul_add,
  ← mul_assoc, add_mul, mul_add (unsym (a * a)), ← add_assoc, ← mul_assoc, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑sym
      (⅟2 * ⅟2 *
        (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
            ↑unsym (a * a) * ↑unsym a * ↑unsym b +
          ↑unsym (a * a) * ↑unsym b * ↑unsym a)) =
    ↑sym
      (⅟2 *
        (↑unsym a * ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) +
          ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) * ↑unsym a))
[PROOFSTEP]
rw [unsym_sym, sym_inj, ← mul_assoc, ← commute_half_left (unsym a), mul_assoc (⅟2) (unsym a),
  mul_assoc (⅟2) _ (unsym a), ← mul_add, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
        (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
conv_rhs => rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
| ⅟2 * ⅟2 *
    (↑unsym a * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) +
      (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [mul_add (unsym a)]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * (↑unsym b * ↑unsym (a * a)) + ↑unsym a * (↑unsym (a * a) * ↑unsym b) +
        (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b) * ↑unsym a)
[PROOFSTEP]
rw [add_mul, ← add_assoc, ← mul_assoc, ← mul_assoc]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym b * ↑unsym a * ↑unsym (a * a) +
          ↑unsym (a * a) * ↑unsym a * ↑unsym b +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym (a * a) + ↑unsym a * ↑unsym (a * a) * ↑unsym b +
          ↑unsym b * ↑unsym (a * a) * ↑unsym a +
        ↑unsym (a * a) * ↑unsym b * ↑unsym a)
[PROOFSTEP]
rw [unsym_mul_self]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * (↑unsym a * ↑unsym a) + ↑unsym b * ↑unsym a * (↑unsym a * ↑unsym a) +
          ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a) =
    ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * (↑unsym a * ↑unsym a) + ↑unsym a * (↑unsym a * ↑unsym a) * ↑unsym b +
          ↑unsym b * (↑unsym a * ↑unsym a) * ↑unsym a +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, ← mul_assoc, ← mul_assoc, ← sub_eq_zero, ← mul_sub]
[GOAL]
case calc_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ⅟2 * ⅟2 *
      (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
            ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
          ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a -
        (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
            ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
          ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a)) =
    0
[PROOFSTEP]
convert mul_zero (⅟(2 : α) * ⅟(2 : α))
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
          ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a -
      (↑unsym a * ↑unsym b * ↑unsym a * ↑unsym a + ↑unsym a * ↑unsym a * ↑unsym a * ↑unsym b +
          ↑unsym b * ↑unsym a * ↑unsym a * ↑unsym a +
        ↑unsym a * ↑unsym a * ↑unsym b * ↑unsym a) =
    0
[PROOFSTEP]
rw [add_sub_add_right_eq_sub, add_assoc, add_assoc, add_sub_add_left_eq_sub, add_comm, add_sub_add_right_eq_sub,
  sub_eq_zero]
  -- Rearrange RHS
[GOAL]
case calc_3
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ ↑sym
      (⅟2 *
        (↑unsym a * ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) +
          ↑unsym (↑sym (⅟2 * (↑unsym b * ↑unsym (a * a) + ↑unsym (a * a) * ↑unsym b))) * ↑unsym a)) =
    a * (b * (a * a))
[PROOFSTEP]
rw [← mul_def, ← mul_def]