awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ degree (T R 0) = (↑(Int.natAbs 0) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ degree (T R 1) = (↑(Int.natAbs 1) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
rw : HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1 = (↑(n + 2) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)

Tactic:
rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih1]

Premises used: mul_assoc, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : n + 1 + 1 = n + 2
⊢ HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1 = (↑(n + 2) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)

Tactic:
have : (2 * X * T R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih1]
      norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
add_two :
  (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
add_two₁ : degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
⊢ degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)

Tactic:
rw [T_add_two, degree_sub_eq_left_of_degree_lt]

Premises used: Polynomial.degree_sub_eq_left_of_degree_lt, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
add_two : Eq (α := WithBot ℕ) (↑(n + 2) : WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
add_two add_two₁ add_two₂ add_two₃ : n + 2 = n + 2
⊢ Eq (α := WithBot ℕ) (↑(n + 2) : WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
add_two : LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) (↑(n + 2) : WithBot ℕ)
⊢ degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree

Tactic:
rw [ih2, this]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) (↑(n + 2) : WithBot ℕ)

Tactic:
tauto
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
ih : degree (T R n) = (↑n.natAbs : WithBot ℕ)
⊢ degree (T R (-n)) = (↑(-n).natAbs : WithBot ℕ)

Tactic:
simp [ih]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
zero : degree (T R 0) = (↑(Int.natAbs 0) : WithBot ℕ)
one : degree (T R 1) = (↑(Int.natAbs 1) : WithBot ℕ)
add_two :
  ∀ (n : ℕ) (ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ))
    (ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)),
    degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
neg : ∀ (n : ℤ) (ih : degree (T R n) = (↑n.natAbs : WithBot ℕ)), degree (T R (-n)) = (↑(-n).natAbs : WithBot ℕ)
⊢ degree (T R n) = (↑n.natAbs : WithBot ℕ)

Tactic:
induction n using Chebyshev.induct' with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : (2 * X * T R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih1]
      norm_cast
    rw [T_add_two, degree_sub_eq_left_of_degree_lt]
    · rw [this]; norm_cast
    · rw [ih2, this]; tauto
  | neg n ih => simp [ih]

Premises used: Polynomial.degree_sub_eq_left_of_degree_lt, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
⊢ natDegree (T R n) = n.natAbs

Tactic:
natDegree_eq_of_degree_eq_some (degree_T R n)

Premises used: Polynomial.Chebyshev.degree_T, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ leadingCoeff (T R 0) = HPow.hPow (α := R) 2 (Int.natAbs 0 - 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ leadingCoeff (T R 1) = HPow.hPow (α := R) 2 (Int.natAbs 1 - 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
change : Eq.{u_1 + 1} (α := R) (leadingCoeff ((C : (a : R) → R[X]) 2)) 2
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2

Tactic:
change leadingCoeff (C 2) = 2

Premises used: Polynomial.C, Polynomial.leadingCoeff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
rw rw₁ : Eq.{u_1 + 1} (α := R) 2 2
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff ((C : (a : R) → R[X]) 2)) 2

Tactic:
rw [leadingCoeff_C]

Premises used: Polynomial.leadingCoeff_C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2

Tactic:
have : leadingCoeff (2 : R[X]) = 2 := by
      change leadingCoeff (C 2) = 2
      rw [leadingCoeff_C]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
add_two :
  HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1) =
    HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)
add_two₁ : degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
⊢ leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)

Tactic:
rw [T_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih1,
      leadingCoeff_mul, leadingCoeff_X, this]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_X, Polynomial.leadingCoeff_sub_of_degree_lt, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
add_two :
  Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1 - 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 (n + 2 - 1)) : R)
⊢ HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1) =
    HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
⊢ Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1 - 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 (n + 2 - 1)) : R)

Tactic:
simp [pow_add, mul_comm]

Premises used: pow_add, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
add_two :
  (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) <
    HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1
⊢ degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree

Tactic:
rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, degree_T,
        degree_T]

Premises used: mul_assoc, Polynomial.Chebyshev.degree_T, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 :
  leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1)
ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
⊢ (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) <
    HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1

Tactic:
tauto
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
ih : leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)
⊢ leadingCoeff (T R (-n)) = HPow.hPow (α := R) 2 ((-n).natAbs - 1)

Tactic:
simp [ih]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
zero : leadingCoeff (T R 0) = HPow.hPow (α := R) 2 (Int.natAbs 0 - 1)
one : leadingCoeff (T R 1) = HPow.hPow (α := R) 2 (Int.natAbs 1 - 1)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs - 1))
    (ih2 : leadingCoeff (T R (↑n : ℤ)) = HPow.hPow (α := R) 2 (Int.natAbs (↑n : ℤ) - 1)),
    leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)
neg :
  ∀ (n : ℤ) (ih : leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)),
    leadingCoeff (T R (-n)) = HPow.hPow (α := R) 2 ((-n).natAbs - 1)
⊢ leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)

Tactic:
induction n using Chebyshev.induct' with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : leadingCoeff (2 : R[X]) = 2 := by
      change leadingCoeff (C 2) = 2
      rw [leadingCoeff_C]
    rw [T_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih1,
      leadingCoeff_mul, leadingCoeff_X, this]
    · norm_cast; simp [pow_add, mul_comm]
    · rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, degree_T,
        degree_T]
      tauto
  | neg n ih => simp [ih]

Premises used: Polynomial.leadingCoeff_mul, mul_assoc, pow_add, Polynomial.Chebyshev.degree_T, Polynomial.leadingCoeff_X, Polynomial.leadingCoeff_sub_of_degree_lt, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ eval (-x) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * eval x (T R 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ eval (-x) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * eval x (T R 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 :
  eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : eval (-x) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ))
trans :
  eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ)))
trans₁ :
  (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ))) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
⊢ eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)

Premises used: Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.T, HSub.hSub, Nat.cast, HAdd.hAdd, OfNat.ofNat, Int.negOnePow
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 :
  eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : eval (-x) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ))
simp :
  -(2 * x) * (-(↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ)) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ)))
⊢ eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ)))

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]

Premises used: Int.cast_neg, even_two, Polynomial.eval_X, Int.negOnePow_add, Polynomial.eval_mul, Int.negOnePow_one, Units.val_neg, Int.negOnePow_even, Polynomial.eval_ofNat, Polynomial.Chebyshev.T_add_two, OfNat.ofNat, Polynomial.eval_sub, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 :
  eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : eval (-x) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ))
⊢ -(2 * x) * (-(↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ)) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ)))

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 :
  eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : eval (-x) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ))
⊢ (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (T R (↑n : ℤ))) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℤ
ih : eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)
⊢ eval (-x) (T R (-n)) = (↑(↑(-n).negOnePow : ℤ) : R) * eval x (T R (-n))

Tactic:
simp [ih]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
x : R
zero : eval (-x) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * eval x (T R 0)
one : eval (-x) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * eval x (T R 1)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
    (ih2 : eval (-x) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (T R (↑n : ℤ))),
    eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
neg :
  ∀ (n : ℤ) (ih : eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)),
    eval (-x) (T R (-n)) = (↑(↑(-n).negOnePow : ℤ) : R) * eval x (T R (-n))
⊢ eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)

Tactic:
induction n using Chebyshev.induct' with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)
    · simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, ih1, Int.negOnePow_add,
        Int.negOnePow_one, Units.val_neg, Int.cast_neg, ih2, Int.negOnePow_even 2 even_two]
      ring_nf
    · simp
  | neg n ih => simp [ih]

Premises used: Int.cast_neg, Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.T, even_two, Polynomial.eval_X, HSub.hSub, Int.negOnePow_add, Polynomial.eval_mul, Int.negOnePow_one, Units.val_neg, HAdd.hAdd, Int.negOnePow_even, Polynomial.eval_ofNat, Polynomial.Chebyshev.T_add_two, OfNat.ofNat, Polynomial.eval_sub, Int.negOnePow, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ degree (T R n) ≠ ⊥

Tactic:
simp [degree_T R n]

Premises used: Polynomial.Chebyshev.degree_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : IsDomain R
inst_3 : NeZero.{u_1} (R := R) 2
n : ℕ
⊢ degree (T R (↑n : ℤ)) = (↑n : WithBot ℕ)

Tactic:
simp [degree_T]

Premises used: Polynomial.Chebyshev.degree_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a :
  U R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) 2 X * U R (-(↑k : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) 2 X * U R (-(↑k : ℤ)) =
    0
⊢ U R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) 2 X * U R (-(↑k : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - U R (-(↑(k + 1) : ℤ)) +
        U 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 : ℕ
⊢ U R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) 2 X * U R (-(↑k : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) 2 X * U R (-(↑k : ℤ)) =
    0

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

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

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

Tactic:
ring_nf