awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ C R (-2) = HPow.hPow (α := R[X]) (β := ℕ) X 2 - 2

Tactic:
simp [C_two]

Premises used: Polynomial.Chebyshev.C_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ comp (C R 0) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ comp (C R 1) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : comp (C R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ))
add_two :
  HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ)) =
    2 * (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ))
⊢ comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]

Premises used: Polynomial.X_comp, Polynomial.mul_comp, Polynomial.Chebyshev.C_add_two, Polynomial.Chebyshev.T_add_two, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : comp (C R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ))
⊢ HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
      HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ)) =
    2 * (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ))

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (C R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ)))
ih2 :
  comp (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
neg_add_one :
  HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ))) -
      HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    2 * (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
⊢ comp (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))

Tactic:
simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Premises used: Polynomial.X_comp, Polynomial.Chebyshev.C_sub_one, Polynomial.Chebyshev.T_sub_one, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (C R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ)))
ih2 :
  comp (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
⊢ HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ))) -
      HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    2 * (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (C R 0) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 0)
one : comp (C R 1) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 1)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) =
        HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
    (ih2 : comp (C R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ))),
    comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
      HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
neg_add_one :
  ∀ (n : ℕ) (ih1 : comp (C R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ))))
    (ih2 :
      comp (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
        HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))),
    comp (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
      HMul.hMul (α := R[X]) 2 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
⊢ comp (C R n) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R n)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring

Premises used: Polynomial.X_comp, Polynomial.Chebyshev.C_sub_one, Polynomial.Chebyshev.T_sub_one, Polynomial.mul_comp, Polynomial.Chebyshev.C_add_two, Polynomial.Chebyshev.T_add_two, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 2 (C R 0) = 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 2 (C R 1) = 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 2
ih2 : eval 2 (C R (↑n : ℤ)) = 2
add_two : HMul.hMul (α := R) 2 2 - 2 = 2
⊢ eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 2

Tactic:
simp [C_add_two, ih1, ih2]

Premises used: Polynomial.Chebyshev.C_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 2
ih2 : eval 2 (C R (↑n : ℤ)) = 2
⊢ HMul.hMul (α := R) 2 2 - 2 = 2

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (C R (-(↑n : ℤ))) = 2
ih2 : eval 2 (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 2
neg_add_one : HMul.hMul (α := R) 2 2 - 2 = 2
⊢ eval 2 (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 2

Tactic:
simp [C_sub_one, -C_neg, ih1, ih2]

Premises used: Polynomial.Chebyshev.C_sub_one, Polynomial.Chebyshev.C_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (C R (-(↑n : ℤ))) = 2
ih2 : eval 2 (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 2
⊢ HMul.hMul (α := R) 2 2 - 2 = 2

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 2 (C R 0) = 2
one : eval 2 (C R 1) = 2
add_two :
  ∀ (n : ℕ) (ih1 : eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 2) (ih2 : eval 2 (C R (↑n : ℤ)) = 2),
    eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 2
neg_add_one :
  ∀ (n : ℕ) (ih1 : eval 2 (C R (-(↑n : ℤ))) = 2) (ih2 : eval 2 (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 2),
    eval 2 (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 2
⊢ eval 2 (C R n) = 2

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [C_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [C_sub_one, -C_neg, ih1, ih2]; norm_num

Premises used: Polynomial.Chebyshev.C_sub_one, Polynomial.Chebyshev.C_neg, Polynomial.Chebyshev.C_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-2) (C R 0) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 0) : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-2) (C R 1) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 1) : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-2) (C R (↑n : ℤ)) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
add_two :
  2 * HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) -
      HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)
⊢ eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)

Tactic:
simp only [C_add_two, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, neg_neg, Polynomial.eval_mul, Int.negOnePow_one, Int.negOnePow_def, Units.val_neg, neg_mul, mul_one, Polynomial.Chebyshev.C_add_two, OfNat.ofNat, Polynomial.eval_sub, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-2) (C R (↑n : ℤ)) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
add_two :
  Eq.{u_1 + 1} (α := R) (↑(2 * (2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) - 2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) : R)
    (↑(2 * (↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ)) : R)
⊢ 2 * HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) -
      HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-2) (C R (↑n : ℤ)) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
add_two : 2 * (2 * HPow.hPow (α := R) (-1) n) - 2 * HPow.hPow (α := R) (-1) n = 2 * HPow.hPow (α := R) (-1) n
⊢ Eq.{u_1 + 1} (α := R) (↑(2 * (2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) - 2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) : R)
    (↑(2 * (↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ)) : R)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-2) (C R (↑n : ℤ)) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
⊢ 2 * (2 * HPow.hPow (α := R) (-1) n) - 2 * HPow.hPow (α := R) (-1) n = 2 * HPow.hPow (α := R) (-1) n

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-2) (C R (-(↑n : ℤ))) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
ih2 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
neg_add_one :
  -(2 * HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)) +
      HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) =
    -HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
⊢ eval (-2) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)

Tactic:
simp only [C_sub_one, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, Polynomial.eval_mul, Int.negOnePow_one, Polynomial.Chebyshev.C_sub_one, Units.val_neg, Int.negOnePow_sub, neg_mul, mul_one, Polynomial.eval_sub, sub_neg_eq_add, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-2) (C R (-(↑n : ℤ))) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
ih2 :
  eval (-2) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
⊢ -(2 * HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)) +
      HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) =
    -HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval (-2) (C R 0) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 0) : ℤ) : R)
one : eval (-2) (C R 1) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 1) : ℤ) : R)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R))
    (ih2 : eval (-2) (C R (↑n : ℤ)) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)),
    eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)
neg_add_one :
  ∀ (n : ℕ) (ih1 : eval (-2) (C R (-(↑n : ℤ))) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R))
    (ih2 :
      eval (-2) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
        HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)),
    eval (-2) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
      HMul.hMul (α := R) 2 (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
⊢ eval (-2) (C R n) = HMul.hMul (α := R) 2 (↑(↑n.negOnePow : ℤ) : R)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [C_add_two, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [C_sub_one, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
    ring

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, neg_neg, Polynomial.eval_mul, Int.negOnePow_one, Int.negOnePow_def, Polynomial.Chebyshev.C_sub_one, Units.val_neg, Int.negOnePow_sub, neg_mul, mul_one, Polynomial.Chebyshev.C_add_two, OfNat.ofNat, Polynomial.eval_sub, sub_neg_eq_add, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
⊢ Eq.{u_1 + 1} (α := R[X])
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (comp (C R n) (HMul.hMul (α := R[X]) 2 X)))
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (HMul.hMul (α := R[X]) 2 (T R n)))

Tactic:
have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (C_comp_two_mul_X R n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
this :
  Eq.{u_1 + 1} (α := R[X])
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (comp (C R n) (HMul.hMul (α := R[X]) 2 X)))
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (HMul.hMul (α := R[X]) 2 (T R n)))
⊢ C R n =
    2 *
      comp (T R n)
        (HMul.hMul (α := R[X])
          ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
    Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X, map_ofNat] at this

Premises used: Nat.cast_ofNat, Polynomial.comp_assoc, Polynomial.X_comp, Polynomial.C_eq_natCast, mul_assoc, map_ofNat, Polynomial.comp_X, map_one, Polynomial.C_mul, Polynomial.ofNat_comp, Polynomial.mul_comp, mul_invOf_self', one_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
this :
  C R n =
    2 *
      comp (T R n)
        (HMul.hMul (α := R[X])
          ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)
⊢ C R n =
    2 *
      comp (T R n)
        (HMul.hMul (α := R[X])
          ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
rw :
  T R n =
    (Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      HMul.hMul (α := R[X]) 2 (T R n)
rw₁ :
  T R n =
    HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) 2 *
      T R n
rw₂ :
  T R n =
    HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _))
        ((Polynomial.C : (a : R) → R[X]) (OfNat.ofNat 2)) *
      T R n
rw₃ :
  T R n =
    HMul.hMul (α := R[X]) (β := R[X])
      ((Polynomial.C : (a : R) → R[X])
          (HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (OfNat.ofNat 2)) :
        R[X])
      (T R n)
rw₄ : T R n = HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) 1) (T R n)
rw₅ : T R n = HMul.hMul (α := R[X]) 1 (T R n)
rw₆ rw₇ : Eq (α := R[X]) (T R n) (T R n)
⊢ T R n =
    (Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
      comp (C R n) (HMul.hMul (α := R[X]) 2 X)

Tactic:
rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]

Premises used: Polynomial.C, mul_assoc, map_ofNat, map_mul, map_one, Polynomial.Chebyshev.C_comp_two_mul_X, invOf_mul_self', OfNat.ofNat, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a :
  S R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) =
    0
⊢ S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - S R (-(↑(k + 1) : ℤ)) +
        S R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Premises used: Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ S R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a :
  S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) X (S R (-(↑k : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - S R (-(↑(k + 1) : ℤ)) +
        S R (Int.negSucc k)) =
    0
⊢ S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - S R (-(↑(k + 1) : ℤ))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) S.eq_4 R k

Premises used: Int.negSucc_eq, Polynomial.Chebyshev.S.eq_4
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n + 1) + (HMul.hMul (α := R[X]) X (S R (n - 1 + 1)) - S R (n - 1)) -
      (HMul.hMul (α := R[X]) X (S R n) - S R (n - 1) + S R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  S R (n + 1) + (HMul.hMul (α := R[X]) X (S R (n - 1 + 1)) - S R (n - 1)) -
      (HMul.hMul (α := R[X]) X (S R n) - S R (n - 1) + S R (n - 1 + 2)) =
    0
⊢ S R (n + 1) = HMul.hMul (α := R[X]) X (S R n) - S R (n - 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.S_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n - 2) + (HMul.hMul (α := R[X]) X (S R (n - 2 + 1)) - S R (n - 2)) -
      (HMul.hMul (α := R[X]) X (S R (n - 1)) - S R n + S R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  S R (n - 2) + (HMul.hMul (α := R[X]) X (S R (n - 2 + 1)) - S R (n - 2)) -
      (HMul.hMul (α := R[X]) X (S R (n - 1)) - S R n + S R (n - 2 + 2)) =
    0
⊢ S R (n - 2) = HMul.hMul (α := R[X]) X (S R (n - 1)) - S R n

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.S_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n - 1) + (HMul.hMul (α := R[X]) X (S R (n - 1 + 1)) - S R (n - 1)) -
      (HMul.hMul (α := R[X]) X (S R n) - S R (n + 1) + S R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  S R (n - 1) + (HMul.hMul (α := R[X]) X (S R (n - 1 + 1)) - S R (n - 1)) -
      (HMul.hMul (α := R[X]) X (S R n) - S R (n + 1) + S R (n - 1 + 2)) =
    0
⊢ S R (n - 1) = HMul.hMul (α := R[X]) X (S R n) - S R (n + 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.S_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R n + (HMul.hMul (α := R[X]) X (S R (n - 2 + 1)) - S R (n - 2)) -
      (HMul.hMul (α := R[X]) X (S R (n - 1)) - S R (n - 2) + S R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  S R n + (HMul.hMul (α := R[X]) X (S R (n - 2 + 1)) - S R (n - 2)) -
      (HMul.hMul (α := R[X]) X (S R (n - 1)) - S R (n - 2) + S R (n - 2 + 2)) =
    0
⊢ S R n = HMul.hMul (α := R[X]) X (S R (n - 1)) - S R (n - 2)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.S_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R 0) 1

Tactic:
simp [S]

Premises used: Polynomial.Chebyshev.S
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R 1) X

Tactic:
simp [S]

Premises used: Polynomial.Chebyshev.S
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R (-1)) 0

Tactic:
simpa using S_sub_one R 0

Premises used: Polynomial.Chebyshev.S_sub_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ S R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) 0 1)) - S R 0

Tactic:
have := S_add_two R 0
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : S R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) 0 1)) - S R 0
⊢ S R 2 = HMul.hMul (α := R[X]) X X - 1

Tactic:
simp only [zero_add, S_one, S_zero] at this

Premises used: zero_add, Polynomial.Chebyshev.S_zero, Polynomial.Chebyshev.S_one