awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
zero : degree (U R (↑0 : ℤ)) = (↑0 : WithBot ℕ)
one : degree (U R (↑1 : ℤ)) = (↑1 : WithBot ℕ)
⊢ degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
have more : ∀ (n : ℕ) (ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)) (ih2 : degree (U R (↑(n + 1) : ℤ)) = (↑(n + 1) : WithBot ℕ)),
  degree (U R (↑(n + 2) : ℤ)) = (↑(n + 2) : WithBot ℕ)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    norm_cast
    rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    have : (2 * X * U R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]
      norm_cast
    rw [U_add_two, degree_sub_eq_left_of_degree_lt]
    · rw [this]; norm_cast
    · rw [ih1, this]; norm_cast; omega
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
hn : n ≠ -1
⊢ degree (U R n) = (↑((n + 1).natAbs - 1) : WithBot ℕ)
have obtain : ∀ (m : ℕ) (hn : Ne (α := ℤ) (↑m : ℤ) (-1)),
  degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
Tactic: obtain ⟨m, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
hn : n ≠ -1
obtain :
  ∀ (m : ℕ) (hn : Ne (α := ℤ) (↑m : ℤ) (-1)),
    degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R n) = (↑((n + 1).natAbs - 1) : WithBot ℕ)
have obtain₁ : ∀ (m : ℕ) (hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)),
  degree (U R (-(↑m : ℤ))) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: obtain ⟨m, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (↑m : ℤ) (-1)
⊢ degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
have rw : Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
Tactic: rw [degree_U_natCast R m]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (↑m : ℤ) (-1)
⊢ Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
have norm_cast : m = m + 1 - 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)
⊢ degree (U R (-(↑m : ℤ))) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have rw : degree (U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: rw [U_neg, degree_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have trans : degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) = degree (U R (↑m : ℤ))
Tactic: trans (U R m).degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)
trans : degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) = degree (U R (↑m : ℤ))
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have trans₁ : degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: trans (U R m).degree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) = degree (U R (↑m : ℤ))
have e_p : HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2 = (↑m : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)
⊢ degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have rw : Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: rw [degree_U_natCast R m]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)
⊢ Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have norm_cast : m = (Int.negSucc (m + 1) + 1).natAbs - 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1) : ℤ)) (-1)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have succ : ∀ (hn : Ne (α := ℤ) (-(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) (-1)),
  degree (U R (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
Cleared hypotheses: m, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑(m + 1) : ℤ)) (-1)
succ :
  ∀ (hn : Ne (α := ℤ) (-(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) (-1)),
    degree (U R (HSub.hSub (α := ℤ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ) 2)) =
      (↑((HAdd.hAdd (α := ℤ) (-(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have succ₁ : ∀ (m : ℕ) (hn : Ne (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) (-1)),
  degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
Cleared hypotheses: m, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have zero : ∀ (hn : Ne (α := ℤ) (-(↑0 : ℤ)) (-1)),
  degree (U R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: cases m with
    | zero => simp
    | succ m =>
      cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
Cleared hypotheses: m, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)
zero :
  ∀ (hn : Ne (α := ℤ) (-(↑0 : ℤ)) (-1)),
    degree (U R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have succ : ∀ (m : ℕ) (hn : Ne (α := ℤ) (-(↑(m + 1) : ℤ)) (-1)),
  degree (U R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: cases m with
    | zero => simp
    | succ m =>
      cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
Cleared hypotheses: m, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)
⊢ degree (U R (-(↑m : ℤ))) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have case : degree (-U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: case inr =>
    rw [U_neg, degree_neg]
    cases m with
    | zero => simp
    | succ m =>
      cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
m : ℕ
hn : Ne (α := ℤ) (-(↑m : ℤ)) (-1)
case : degree (-U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (-(↑m : ℤ))) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
have case₁ : degree (U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1).natAbs - 1) : WithBot ℕ)
Tactic: case inr =>
    rw [U_neg, degree_neg]
    cases m with
    | zero => simp
    | succ m =>
      cases m with
      | zero => contradiction
      | succ m =>
        trans (U R m).degree
        · congr; omega
        · rw [degree_U_natCast R m]; norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
⊢ natDegree (U R n) = (n + 1).natAbs - 1
have pos : n = -1 → natDegree (U R n) = (n + 1).natAbs - 1
Tactic: by_cases n = -1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
pos : n = -1 → natDegree (U R n) = (n + 1).natAbs - 1
⊢ natDegree (U R n) = (n + 1).natAbs - 1
have neg : ¬n = -1 → natDegree (U R n) = (n + 1).natAbs - 1
Tactic: by_cases n = -1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
hn : n = -1
⊢ natDegree (U R n) = (n + 1).natAbs - 1
have subst : natDegree (U R (-1)) = (HAdd.hAdd (α := ℤ) (-1) 1).natAbs - 1
Tactic: subst hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
have rw : Eq.{u_1 + 1} (α := R) (leadingCoeff ((C : (a : R) → R[X]) 2)) 2
Tactic: rw [← C_ofNat, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (leadingCoeff ((C : (a : R) → R[X]) 2)) 2
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
have rw₁ : Eq.{u_1 + 1} (α := R) 2 2
Tactic: rw [← C_ofNat, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
⊢ leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
have this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
Tactic: have : leadingCoeff (2 : R[X]) = 2 := by
    rw [← C_ofNat, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (↑(n + 1) : ℤ)) = HPow.hPow (α := R) 2 (n + 1)
⊢ leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 (n + 2)
have ih2₁ : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
Tactic: push_cast at ih2
Cleared hypotheses: ih2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
⊢ leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 (n + 2)
have more : HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 (n + 1) = HPow.hPow (α := R) 2 (n + 2)
Tactic: rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
more : HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 (n + 1) = HPow.hPow (α := R) 2 (n + 2)
⊢ leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 (n + 2)
have more₁ : degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
Tactic: rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
⊢ HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 (n + 1) = HPow.hPow (α := R) 2 (n + 2)
have more : Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1)) : R)
  (↑(HPow.hPow (α := ℕ) 2 (n + 2)) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
⊢ Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 (n + 2)) : R)
have more : Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * (HPow.hPow (α := ℕ) 2 n * HPow.hPow (α := ℕ) (β := ℕ) 2 1)) : R)
  (↑(HPow.hPow (α := ℕ) 2 n * HPow.hPow (α := ℕ) (β := ℕ) 2 2) : R)
Tactic: rw [pow_add, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
⊢ degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (↑(n + 1) : ℤ)).degree
have more : (↑n : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑(n + 1) : WithBot ℕ) 1
Tactic: rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
n : ℕ
ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
ih2 : leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)
⊢ (↑n : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑(n + 1) : WithBot ℕ) 1
have more : n < n + 1 + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
⊢ leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
have zero : leadingCoeff (U R (↑0 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 0
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp [this]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]
    · norm_cast; rw [pow_add, pow_add]; ring_nf
    · norm_cast
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]
      norm_cast; omega
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
zero : leadingCoeff (U R (↑0 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 0
⊢ leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
have one : leadingCoeff (U R (↑1 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 1
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp [this]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]
    · norm_cast; rw [pow_add, pow_add]; ring_nf
    · norm_cast
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]
      norm_cast; omega
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
this : Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2
zero : leadingCoeff (U R (↑0 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 0
one : leadingCoeff (U R (↑1 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 1
⊢ leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n
have more : ∀ (n : ℕ) (ih1 : leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n)
  (ih2 : leadingCoeff (U R (↑(n + 1) : ℤ)) = HPow.hPow (α := R) 2 (n + 1)),
  leadingCoeff (U R (↑(n + 2) : ℤ)) = HPow.hPow (α := R) 2 (n + 2)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp [this]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]
    · norm_cast; rw [pow_add, pow_add]; ring_nf
    · norm_cast
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X,
        degree_U_natCast R n, degree_U_natCast R (n + 1)]
      norm_cast; omega
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
ih2 : eval (-x) (U R (↑(n + 1) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 1) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 1) : ℤ))
⊢ eval (-x) (U R (↑(n + 2) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 2) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 2) : ℤ))
have trans : eval (-x) (U R (↑(n + 2) : ℤ)) =
  (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
    (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
Tactic: trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
ih2 : eval (-x) (U R (↑(n + 1) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 1) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 1) : ℤ))
trans :
  eval (-x) (U R (↑(n + 2) : ℤ)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
⊢ eval (-x) (U R (↑(n + 2) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 2) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 2) : ℤ))
have trans₁ : (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
    (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ))) =
  (↑(↑(Int.negOnePow (↑(n + 2) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 2) : ℤ))
Tactic: trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
ih2 : eval (-x) (U R (↑(n + 1) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 1) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 1) : ℤ))
⊢ eval (-x) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
have ih2₁ : eval (-x) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
  (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
Tactic: push_cast at ih2
Cleared hypotheses: ih2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
ih2 :
  eval (-x) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
⊢ eval (-x) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
have rw : eval (-x) 2 * eval (-x) X * ((↑(↑(-Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
    (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ)) =
  (↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) *
    (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
Tactic: rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
n : ℕ
ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
ih2 :
  eval (-x) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
⊢ eval (-x) 2 * eval (-x) X * ((↑(↑(-Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ)) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * 1) : ℤ) : R) *
      (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
have simp : 2 * x * (HPow.hPow (α := R) (-1) n * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
    HPow.hPow (α := R) (-1) n * eval x (U R (↑n : ℤ)) =
  HPow.hPow (α := R) (-1) n * (2 * x * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - eval x (U R (↑n : ℤ)))
Tactic: simp