awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (U R 0) = U R' 0
one : map f (U R 1) = U R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)),
    map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg_add_one :
  ∀ (n : ℕ) (ih1 : map f (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ)))
    (ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
    map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R n) = U R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Premises used: Polynomial.map_mul, Polynomial.Chebyshev.U_sub_one, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.Chebyshev.U_add_two, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (C R 0) = C R' 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (C R 1) = C R' 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₂ :
  map f X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₃ :
  X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)

Tactic:
simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_sub, Polynomial.Chebyshev.C_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ)))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.Chebyshev.C_sub_one, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (C R 0) = C R' 0
one : map f (C R 1) = C R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)),
    map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg_add_one :
  ∀ (n : ℕ) (ih1 : map f (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ)))
    (ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
    map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R n) = C R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.Chebyshev.C_sub_one, Polynomial.map_sub, Polynomial.Chebyshev.C_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (S R 0) = S R' 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (S R 1) = S R' 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₂ :
  map f X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₃ :
  X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)

Tactic:
simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_sub, Polynomial.Chebyshev.S_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.Chebyshev.S_sub_one, Polynomial.map_X, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (S R 0) = S R' 0
one : map f (S R 1) = S R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)),
    map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg_add_one :
  ∀ (n : ℕ) (ih1 : map f (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ)))
    (ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
    map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R n) = S R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.Chebyshev.S_sub_one, Polynomial.map_X, Polynomial.map_sub, Polynomial.Chebyshev.S_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (T R n) = eval x (T R' n)
rw₁ : eval x (map (algebraMap R R') (T R n)) = eval x (T R' n)
rw₂ rw₃ : eval x (T R' n) = eval x (T R' n)
⊢ (aeval x : (a : R[X]) → R') (T R n) = eval x (T R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_T]

Premises used: Polynomial.aeval_def, Polynomial.Chebyshev.map_T, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (U R n) = eval x (U R' n)
rw₁ : eval x (map (algebraMap R R') (U R n)) = eval x (U R' n)
rw₂ rw₃ : eval x (U R' n) = eval x (U R' n)
⊢ (aeval x : (a : R[X]) → R') (U R n) = eval x (U R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_U]

Premises used: Polynomial.aeval_def, Polynomial.Chebyshev.map_U, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (C R n) = eval x (C R' n)
rw₁ : eval x (map (algebraMap R R') (C R n)) = eval x (C R' n)
rw₂ rw₃ : eval x (C R' n) = eval x (C R' n)
⊢ (aeval x : (a : R[X]) → R') (C R n) = eval x (C R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_C]

Premises used: Polynomial.aeval_def, Polynomial.Chebyshev.map_C, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (S R n) = eval x (S R' n)
rw₁ : eval x (map (algebraMap R R') (S R n)) = eval x (S R' n)
rw₂ rw₃ : eval x (S R' n) = eval x (S R' n)
⊢ (aeval x : (a : R[X]) → R') (S R n) = eval x (S R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_S]

Premises used: Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map, Polynomial.Chebyshev.map_S
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (T R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (T R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Polynomial.Chebyshev.aeval_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (U R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (U R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Polynomial.Chebyshev.aeval_U
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (C R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (C R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Polynomial.Chebyshev.aeval_C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (S R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (S R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Polynomial.Chebyshev.aeval_S
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ (derivative : (a : R[X]) → R[X]) (T R 0) = HMul.hMul (α := R[X]) (↑0 : R[X]) (U R (HSub.hSub (α := ℤ) 0 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ (derivative : (a : R[X]) → R[X]) (T R 1) = HMul.hMul (α := R[X]) (↑1 : R[X]) (U R (HSub.hSub (α := ℤ) 1 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])

Tactic:
have h₁ := congr_arg derivative (T_add_two R n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
⊢ U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
have h₂ := U_sub_one R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))

Tactic:
have h₃ := T_eq_U_sub_X_mul_U R (n + 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HSub.hSub (β := R[X])
      ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
          ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
      ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])

Tactic:
simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁

Premises used: Polynomial.derivative_mul, Polynomial.derivative_ofNat, Polynomial.derivative_X, Polynomial.derivative_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
h₁ :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HSub.hSub (β := R[X])
      ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
          ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
      ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])
⊢ HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
        (HAdd.hAdd (β := R[X])
                (HSub.hSub (β := R[X])
                  ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
                    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
                      ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
                  ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X]))
                ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X]) +
              HMul.hMul (α := R[X]) 2 X *
                (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) +
            2 *
              (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) -
                HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))) +
          HMul.hMul (α := R[X]) (↑n : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))) -
      (HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
        (HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
                (HMul.hMul (α := R[X]) (↑n : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))) +
              HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
                ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]) +
            HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
          (↑n : R[X]) * (HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
    0

Tactic:
ring_nf