case zero
R : Type ?u.109021
A : Type ?u.109024
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (U ℂ Nat.zero) * sin θ = sin ((↑Nat.zero + 1) * θ)

case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ)
R : Type ?u.109021
A : Type ?u.109024
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
n : ℕ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)
induction' n with d hd
no goals
case zero
R : Type ?u.109021
A : Type ?u.109024
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
θ : ℂ
⊢ eval (cos θ) (U ℂ Nat.zero) * sin θ = sin ((↑Nat.zero + 1) * θ)
simp [U_zero, eval_one, zero_add, one_mul, Nat.zero_eq, CharP.cast_eq_zero]
case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ)
case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ)
rw [U_eq_X_mul_U_add_T]
case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ + θ)
case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ)
simp only [eval_add, eval_mul, eval_X, T_complex_cos, add_mul, mul_assoc, hd, one_mul]
R : Type ?u.109021
A : Type ?u.109024
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.109021
A : Type ?u.109024
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) * θ + θ)
case succ
R : Type ?u.109021
A : Type ?u.109024
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) * θ + θ)
trans cos θ * sin (↑(d.succ) * θ) + cos (↑(d.succ) * θ) * sin θ
R : Type ?u.109021
A : Type ?u.109024
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) * θ + θ)

R : Type ?u.109021
A : Type ?u.109024
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.109021
A : Type ?u.109024
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.109021
A : Type ?u.109024
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) * θ + θ)
swap
R : Type ?u.109021
A : Type ?u.109024
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 θ
R : Type ?u.109021
A : Type ?u.109024
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 θ
push_cast
no goals
R : Type ?u.109021
A : Type ?u.109024
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 θ
simp only [add_mul, one_mul]
no goals
R : Type ?u.109021
A : Type ?u.109024
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) * θ + θ)
conv_rhs => rw [sin_add, mul_comm]