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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 0 1)) =
    HMul.hMul (α := R[X]) X (S R 0) + C R (HAdd.hAdd (α := ℤ) 0 1)
one :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 1 1)) =
    HMul.hMul (α := R[X]) X (S R 1) + C R (HAdd.hAdd (α := ℤ) 1 1)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
        HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1))
    (ih2 :
      HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)),
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (n + 1)) = HMul.hMul (α := R[X]) X (S R n) + C R (n + 1)
have neg_add_one : ∀ (n : ℕ)
  (ih1 :
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
      HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
  (ih2 :
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)),
  HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [S_two, C_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := S_add_two R (n + 1)
    have h₂ := S_add_two R n
    have h₃ := C_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_add_two R (-n - 1)
    have h₂ := S_add_two R (-n)
    have h₃ := C_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (X : R[X]) * ih1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ C R n = HMul.hMul (α := R[X]) 2 (S R n) - HMul.hMul (α := R[X]) X (S R (n - 1))
have a : C R n + HMul.hMul (α := R[X]) 2 (S R (n - 1 + 1)) -
    (HMul.hMul (α := R[X]) 2 (S R n) - HMul.hMul (α := R[X]) X (S R (n - 1)) +
      (HMul.hMul (α := R[X]) X (S R (n - 1)) + C R (n - 1 + 1))) =
  0
Tactic: linear_combination (norm := ring_nf) - S_eq_X_mul_S_add_C R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two : map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₁ : map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₂ : map f 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₃ : 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₃ :
  2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₄ : HMul.hMul (α := R'[X]) 2 X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₃ :
  2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₅ : HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - map f (T R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
Tactic: simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one : map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₁ : map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₂ : map f 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₃ : 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₄ : HMul.hMul (α := R'[X]) 2 X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₅ : HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
⊢ map f (T R n) = T R' n
have zero : map f (T R 0) = T R' 0
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (T R 0) = T R' 0
⊢ map f (T R n) = T R' n
have one : map f (T R 1) = T R' 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (T R 0) = T R' 0
one : map f (T R 1) = T R' 1
⊢ map f (T R n) = T R' n
have add_two : ∀ (n : ℕ) (ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
  (ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)),
  map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (T R 0) = T R' 0
one : map f (T R 1) = T R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)),
    map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
⊢ map f (T R n) = T R' n
have neg_add_one : ∀ (n : ℕ) (ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ)))
  (ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
  map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 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 [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two : map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
Tactic: simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₁ : map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
Tactic: simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₂ : map f 2 * map f X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
Tactic: simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₃ : 2 * map f X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
Tactic: simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]