awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
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 : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₄ : HMul.hMul (α := R'[X]) 2 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 : ℤ)
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 : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) 2 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₅ : 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 (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one : map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₁ : map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₂ : map f 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₃ : 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₄ : HMul.hMul (α := R'[X]) 2 X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₅ : HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_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 (U R n) = U R' n
have zero : map f (U R 0) = U R' 0
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_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 (U R 0) = U R' 0
⊢ map f (U R n) = U R' n
have one : map f (U R 1) = U R' 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_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 (U R 0) = U R' 0
one : map f (U R 1) = U R' 1
⊢ map f (U R n) = U R' n
have add_two : ∀ (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)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_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 (U R 0) = U R' 0
one : map f (U R 1) = U R' 1
add_two :
  ∀ (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)
⊢ map f (U R n) = U R' n
have neg_add_one : ∀ (n : ℕ) (ih1 : map f (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ)))
  (ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
  map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [U_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 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two : map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
Tactic: simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₁ : map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (C R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
Tactic: simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₂ : map f X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
Tactic: simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₂ :
  map f X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₃ : X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
Tactic: simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (C R (↑n : ℤ)) = C R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₂ :
  map f X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
add_two₃ :
  X * map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
⊢ map f (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₄ : HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (C R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (C R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R' (↑n : ℤ)
Tactic: simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one : map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₁ : map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ)))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ)))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₂ : map f X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ)))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₃ : X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R (-(↑n : ℤ))) = C R' (-(↑n : ℤ))
ih2 : map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ)))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  X * map f (C R (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = C R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₄ : HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - map f (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (C R' (-(↑n : ℤ))) - C R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]