[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
n : ℕ
⊢ ↑(aeval x) (T R n) = eval x (T A n)
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, map_T]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
n : ℕ
⊢ ↑(aeval x) (U R n) = eval x (U A n)
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, map_U]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : R
n : ℕ
⊢ ↑(algebraMap R A) (eval x (T R n)) = eval (↑(algebraMap R A) x) (T A n)
[PROOFSTEP]
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : R
n : ℕ
⊢ ↑(algebraMap R A) (eval x (U R n)) = eval (↑(algebraMap R A) x) (U A n)
[PROOFSTEP]
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos (↑0 * θ)
[PROOFSTEP]
simp only [T_zero, eval_one, Nat.cast_zero, zero_mul, cos_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (T ℂ 1) = cos (↑1 * θ)
[PROOFSTEP]
simp only [eval_X, one_mul, T_one, Nat.cast_one]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
[PROOFSTEP]
have : (2 : ℂ[X]) = (2 : ℕ) := by norm_num
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ 2 = ↑2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ eval (cos θ) (T ℂ (n + 2)) = cos (↑(n + 2) * θ)
[PROOFSTEP]
simp only [this, eval_X, eval_one, T_add_two, eval_sub, eval_mul, eval_nat_cast]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ ↑2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos (↑(n + 2) * θ)
[PROOFSTEP]
simp only [Nat.cast_ofNat, Nat.cast_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * eval (cos θ) (T ℂ (n + 1)) - eval (cos θ) (T ℂ n) = cos ((↑n + 2) * θ)
[PROOFSTEP]
rw [T_complex_cos (n + 1), T_complex_cos n]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * cos θ * cos (↑(n + 1) * θ) - cos (↑n * θ) = cos ((↑n + 2) * θ)
[PROOFSTEP]
simp only [Nat.cast_add, Nat.cast_one, add_mul, cos_add, one_mul, mul_assoc, sin_two_mul, cos_two_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
this : 2 = ↑2
⊢ 2 * (cos θ * (cos (↑n * θ) * cos θ - sin (↑n * θ) * sin θ)) - cos (↑n * θ) =
    cos (↑n * θ) * (2 * cos θ ^ 2 - 1) - sin (↑n * θ) * (2 * (sin θ * cos θ))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (U ℂ Nat.zero) * sin θ = sin ((↑Nat.zero + 1) * θ)
[PROOFSTEP]
simp [U_zero, eval_one, zero_add, one_mul, Nat.zero_eq, CharP.cast_eq_zero]
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ eval (cos θ) (U ℂ (Nat.succ d)) * sin θ = sin ((↑(Nat.succ d) + 1) * θ)
[PROOFSTEP]
rw [U_eq_X_mul_U_add_T]
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ eval (cos θ) (X * U ℂ d + T ℂ (d + 1)) * sin θ = sin ((↑(Nat.succ d) + 1) * θ)
[PROOFSTEP]
simp only [eval_add, eval_mul, eval_X, T_complex_cos, add_mul, mul_assoc, hd, one_mul]
  -- Porting note: added `trans` to prevent `rw` from going on a wild goose chase applying `rfl`
[GOAL]
case succ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
trans cos θ * sin (↑(d.succ) * θ) + cos (↑(d.succ) * θ) * sin θ
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ =
    cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
swap
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ = sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
conv_rhs => rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
| sin (↑(Nat.succ d) * θ + θ)
[PROOFSTEP]
rw [sin_add, mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos (↑(d + 1) * θ) * sin θ =
    cos θ * sin (↑(Nat.succ d) * θ) + cos (↑(Nat.succ d) * θ) * sin θ
[PROOFSTEP]
push_cast
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
d : ℕ
hd : eval (cos θ) (U ℂ d) * sin θ = sin ((↑d + 1) * θ)
⊢ cos θ * sin (↑d * θ + θ) + cos ((↑d + 1) * θ) * sin θ = cos θ * sin ((↑d + 1) * θ) + cos ((↑d + 1) * θ) * sin θ
[PROOFSTEP]
simp only [add_mul, one_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℝ
n : ℕ
⊢ eval (cos θ) (T ℝ n) = cos (↑n * θ)
[PROOFSTEP]
exact_mod_cast T_complex_cos θ n
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℝ
n : ℕ
⊢ eval (cos θ) (U ℝ n) * sin θ = sin ((↑n + 1) * θ)
[PROOFSTEP]
exact_mod_cast U_complex_cos θ n
