awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ)
⊢ degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
have add_two : LT.lt (α := WithBot ℕ) (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) (↑(n + 2) : WithBot ℕ)
Tactic: rw [ih2, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
⊢ degree (T R n) = (↑n.natAbs : WithBot ℕ)
have zero : degree (T R 0) = (↑(Int.natAbs 0) : 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ)
⊢ degree (T R n) = (↑n.natAbs : WithBot ℕ)
have one : degree (T R 1) = (↑(Int.natAbs 1) : 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ)
⊢ degree (T R n) = (↑n.natAbs : WithBot ℕ)
have 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 ℕ)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ)
⊢ degree (T R n) = (↑n.natAbs : WithBot ℕ)
have neg : ∀ (n : ℤ) (ih : 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
have change : Eq.{u_1 + 1} (α := R) (leadingCoeff ((C : (a : R) → R[X]) 2)) 2
Tactic: change leadingCoeff (C 2) = 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ((C : (a : R) → R[X]) 2)) 2
have rw : Eq.{u_1 + 1} (α := R) 2 2
Tactic: rw [leadingCoeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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)
⊢ leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)
have this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
Tactic: have : leadingCoeff (2 : R[X]) = 2 := by
      change leadingCoeff (C 2) = 2
      rw [leadingCoeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)
have 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)
Tactic: rw [T_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih1,
      leadingCoeff_mul, leadingCoeff_X, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ leadingCoeff (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 ((HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs - 1)
have add_two₁ : degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
Tactic: rw [T_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih1,
      leadingCoeff_mul, leadingCoeff_X, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
have add_two : (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ) <
  HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1
Tactic: rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, degree_T,
        degree_T]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
⊢ leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)
have zero : leadingCoeff (T R 0) = HPow.hPow (α := R) 2 (Int.natAbs 0 - 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)
have one : leadingCoeff (T R 1) = HPow.hPow (α := R) 2 (Int.natAbs 1 - 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)
have 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)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ leadingCoeff (T R n) = HPow.hPow (α := R) 2 (n.natAbs - 1)
have 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)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ))
⊢ eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have 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 : ℤ)))
Tactic: trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ)))
⊢ eval (-x) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) * eval x (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have 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))
Tactic: trans (n + 2 : ℤ).negOnePow * (2 * x * (T R (n + 1)).eval x - (T R n).eval x)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ))
⊢ 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 : ℤ)))
have 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 : ℤ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
x : R
⊢ eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)
have zero : eval (-x) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * eval x (T R 0)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)
have one : eval (-x) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * eval x (T R 1)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)
have 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))
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
⊢ eval (-x) (T R n) = (↑(↑n.negOnePow : ℤ) : R) * eval x (T R n)
have 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))
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ 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
have 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
Tactic: simp [Int.negSucc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ U R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - U R (-(↑(k + 1) : ℤ))
have 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
Tactic: linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) U.eq_4 R k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n + 1) = HMul.hMul (α := R[X]) 2 X * U R n - U R (n - 1)
have a : 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: linear_combination (norm := ring_nf) U_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n - 2) = HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R n
have a : U R (n - 2) + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
    (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R n + U R (n - 2 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) U_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n - 1) = HMul.hMul (α := R[X]) 2 X * U R n - U R (n + 1)
have a : 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: linear_combination (norm := ring_nf) U_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R n = HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R (n - 2)
have a : U R n + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
    (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R (n - 2) + U R (n - 2 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) U_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
⊢ U R 2 = 4 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
have this : U R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) 0 1) - U R 0
Tactic: have := U_add_two R 0