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
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))
⊢ comp (C R n) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R n)
have 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))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ eval 2 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 2
have add_two : HMul.hMul (α := R) 2 2 - 2 = 2
Tactic: simp [C_add_two, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ eval 2 (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 2
have neg_add_one : HMul.hMul (α := R) 2 2 - 2 = 2
Tactic: simp [C_sub_one, -C_neg, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 2 (C R n) = 2
have zero : eval 2 (C R 0) = 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 2 (C R 0) = 2
⊢ eval 2 (C R n) = 2
have one : eval 2 (C R 1) = 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 2 (C R 0) = 2
one : eval 2 (C R 1) = 2
⊢ eval 2 (C R n) = 2
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ eval 2 (C R n) = 2
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-2) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R) 2 (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 * 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑(2 * (2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) - 2 * (↑(Int.negOnePow (↑n : ℤ)) : ℤ)) : R)
    (↑(2 * (↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ)) : R)
have add_two : 2 * (2 * HPow.hPow (α := R) (-1) n) - 2 * HPow.hPow (α := R) (-1) n = 2 * HPow.hPow (α := R) (-1) n
Tactic: norm_num
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-2) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R) 2 (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval (-2) (C R n) = HMul.hMul (α := R) 2 (↑(↑n.negOnePow : ℤ) : R)
have zero : eval (-2) (C R 0) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 0) : ℤ) : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval (-2) (C R 0) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 0) : ℤ) : R)
⊢ eval (-2) (C R n) = HMul.hMul (α := R) 2 (↑(↑n.negOnePow : ℤ) : R)
have one : eval (-2) (C R 1) = HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow 1) : ℤ) : 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-2) (C R n) = HMul.hMul (α := R) 2 (↑(↑n.negOnePow : ℤ) : R)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ eval (-2) (C R n) = HMul.hMul (α := R) 2 (↑(↑n.negOnePow : ℤ) : R)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
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)
have 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)))
Tactic: have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (C_comp_two_mul_X R n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
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)
have 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)
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ 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)
have 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
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ 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)
have 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
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ 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)
have 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)
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ 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)
have rw₄ : T R n = HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) 1) (T R n)
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ 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)
have rw₅ : T R n = HMul.hMul (α := R[X]) 1 (T R n)
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ 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)
have rw₆ : Eq (α := R[X]) (T R n) (T R n)
Tactic: rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self',
    map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ 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
have 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
Tactic: simp [Int.negSucc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - S R (-(↑(k + 1) : ℤ))
have 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
Tactic: linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) S.eq_4 R k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n + 1) = HMul.hMul (α := R[X]) X (S R n) - S R (n - 1)
have 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
Tactic: linear_combination (norm := ring_nf) S_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n - 2) = HMul.hMul (α := R[X]) X (S R (n - 1)) - S R n
have 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
Tactic: linear_combination (norm := ring_nf) S_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R (n - 1) = HMul.hMul (α := R[X]) X (S R n) - S R (n + 1)
have 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
Tactic: linear_combination (norm := ring_nf) S_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ S R n = HMul.hMul (α := R[X]) X (S R (n - 1)) - S R (n - 2)
have 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
Tactic: linear_combination (norm := ring_nf) S_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
⊢ S R 2 = HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
have this : 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