case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 2 ^ Nat.zero - y ^ 2 ^ Nat.zero = (∏ i in range Nat.zero, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (∏ i in range (Nat.succ d), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
R : Type u_1
n✝ : ℕ
inst✝ : CommRing R
x y : R
n : ℕ
⊢ x ^ 2 ^ n - y ^ 2 ^ n = (∏ i in range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
induction' n with d hd
no goals
case zero
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 2 ^ Nat.zero - y ^ 2 ^ Nat.zero = (∏ i in range Nat.zero, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul, Nat.zero_eq]
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (∏ i in range (Nat.succ d), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
  rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
no goals
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (∏ i in range (Nat.succ d), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ Nat.succ d - y ^ 2 ^ Nat.succ d = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
rw [Nat.succ_eq_add_one]
no goals
case succ
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i in range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
ring