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 : ℤ
⊢ map f (C R n) = C R' n
have zero : map f (C R 0) = C R' 0
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R 0) = C R' 0
⊢ map f (C R n) = C R' n
have one : map f (C R 1) = C R' 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R 0) = C R' 0
one : map f (C R 1) = C R' 1
⊢ map f (C R n) = C R' n
have add_two : ∀ (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)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (C R 0) = C R' 0
one : map f (C R 1) = C R' 1
add_two :
  ∀ (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)
⊢ map f (C R n) = C R' n
have neg_add_one : ∀ (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)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two : map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
Tactic: simp_rw [S_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 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₁ : map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (S R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
Tactic: simp_rw [S_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 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₂ : map f X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
Tactic: simp_rw [S_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 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₂ :
  map f X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₃ : X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
Tactic: simp_rw [S_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 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₂ :
  map f X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
add_two₃ :
  X * map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
⊢ map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₄ : HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (S R (↑n : ℤ)) =
  HMul.hMul (α := R'[X]) X (S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R' (↑n : ℤ)
Tactic: simp_rw [S_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 (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one : map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [S_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 (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₁ : map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [S_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 (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₂ : map f X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [S_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 (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₃ : X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [S_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 (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ))
ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  X * map f (S R (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₄ : HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  HMul.hMul (α := R'[X]) X (S R' (-(↑n : ℤ))) - S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [S_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 : ℤ
⊢ map f (S R n) = S R' n
have zero : map f (S R 0) = S R' 0
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (S R 0) = S R' 0
⊢ map f (S R n) = S R' n
have one : map f (S R 1) = S R' 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (S R 0) = S R' 0
one : map f (S R 1) = S R' 1
⊢ map f (S R n) = S R' n
have add_two : ∀ (n : ℕ) (ih1 : map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
  (ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)),
  map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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 (S R 0) = S R' 0
one : map f (S R 1) = S R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (S R (↑n : ℤ)) = S R' (↑n : ℤ)),
    map f (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = S R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
⊢ map f (S R n) = S R' n
have neg_add_one : ∀ (n : ℕ) (ih1 : map f (S R (-(↑n : ℤ))) = S R' (-(↑n : ℤ)))
  (ih2 : map f (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
  map f (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = S R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [S_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [S_sub_one, Polynomial.map_sub, Polynomial.map_mul, 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x : (a : R[X]) → R') (T R n) = eval x (T R' n)
have rw : eval₂ (algebraMap R R') x (T R n) = eval x (T R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_T]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (T R n) = eval x (T R' n)
⊢ (aeval x : (a : R[X]) → R') (T R n) = eval x (T R' n)
have rw₁ : eval x (map (algebraMap R R') (T R n)) = eval x (T R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_T]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (T R n) = eval x (T R' n)
rw₁ : eval x (map (algebraMap R R') (T R n)) = eval x (T R' n)
⊢ (aeval x : (a : R[X]) → R') (T R n) = eval x (T R' n)
have rw₂ : eval x (T R' n) = eval x (T R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_T]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x : (a : R[X]) → R') (U R n) = eval x (U R' n)
have rw : eval₂ (algebraMap R R') x (U R n) = eval x (U R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_U]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (U R n) = eval x (U R' n)
⊢ (aeval x : (a : R[X]) → R') (U R n) = eval x (U R' n)
have rw₁ : eval x (map (algebraMap R R') (U R n)) = eval x (U R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_U]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (U R n) = eval x (U R' n)
rw₁ : eval x (map (algebraMap R R') (U R n)) = eval x (U R' n)
⊢ (aeval x : (a : R[X]) → R') (U R n) = eval x (U R' n)
have rw₂ : eval x (U R' n) = eval x (U R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_U]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x : (a : R[X]) → R') (C R n) = eval x (C R' n)
have rw : eval₂ (algebraMap R R') x (C R n) = eval x (C R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_C]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (C R n) = eval x (C R' n)
⊢ (aeval x : (a : R[X]) → R') (C R n) = eval x (C R' n)
have rw₁ : eval x (map (algebraMap R R') (C R n)) = eval x (C R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_C]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (C R n) = eval x (C R' n)
rw₁ : eval x (map (algebraMap R R') (C R n)) = eval x (C R' n)
⊢ (aeval x : (a : R[X]) → R') (C R n) = eval x (C R' n)
have rw₂ : eval x (C R' n) = eval x (C R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_C]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x : (a : R[X]) → R') (S R n) = eval x (S R' n)
have rw : eval₂ (algebraMap R R') x (S R n) = eval x (S R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_S]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (S R n) = eval x (S R' n)
⊢ (aeval x : (a : R[X]) → R') (S R n) = eval x (S R' n)
have rw₁ : eval x (map (algebraMap R R') (S R n)) = eval x (S R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_S]
-- 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'
inst_2 : Algebra R R'
x : R'
n : ℤ
rw : eval₂ (algebraMap R R') x (S R n) = eval x (S R' n)
rw₁ : eval x (map (algebraMap R R') (S R n)) = eval x (S R' n)
⊢ (aeval x : (a : R[X]) → R') (S R n) = eval x (S R' n)
have rw₂ : eval x (S R' n) = eval x (S R' n)
Tactic: rw [aeval_def, eval₂_eq_eval_map, map_S]
-- 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'
inst_2 : Algebra R R'
x : R
n : ℤ
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (T R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
have rw : Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (T R n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]
-- 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'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (T R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (T R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
have rw₁ : Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (T R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]
-- 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'
inst_2 : Algebra R R'
x : R
n : ℤ
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (U R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
have rw : Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (U R n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]
-- 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'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (U R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (U R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
have rw₁ : Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (U R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]