awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
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 ℕ)
⊢ degree (U R (↑n : ℤ)) = (↑n : 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

Premises used: Polynomial.Chebyshev.U_one, Polynomial.Chebyshev.U_add_two, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_sub_eq_left_of_degree_lt, Polynomial.degree_C_mul_X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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

Tactic:
natDegree_eq_of_degree_eq_some (degree_U_natCast R n)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ degree (U R (-1)) = ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ natDegree (U R (-1)) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
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 ℕ)

Tactic:
obtain ⟨m, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
rw : Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)

Tactic:
rw [degree_U_natCast R m]

Premises used: Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = m + 1 - 1
⊢ Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (↑m : ℤ) 1).natAbs - 1) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)

Tactic:
case inl => rw [degree_U_natCast R m]; norm_cast

Premises used: Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
rw : 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 ℕ)

Tactic:
rw [U_neg, degree_neg]

Premises used: Polynomial.Chebyshev.U_neg, Polynomial.degree_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
hn : Ne (α := ℤ) (-(↑0 : ℤ)) (-1)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑0 : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1).natAbs - 1) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
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:
contradiction
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
trans₁ : degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)

Tactic:
trans (U R m).degree

Premises used: Polynomial.Chebyshev.U, Polynomial.degree, Nat.cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
e_p : HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2 = (↑m : ℤ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2)) = degree (U R (↑m : ℤ))

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ HSub.hSub (α := ℤ) (↑(m + 1 + 1) : ℤ) 2 = (↑m : ℤ)

Tactic:
omega
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
rw : Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (↑m : ℤ)) = (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)

Tactic:
rw [degree_U_natCast R m]

Premises used: Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : m = (Int.negSucc (m + 1) + 1).natAbs - 1
⊢ Eq (α := WithBot ℕ) (↑m : WithBot ℕ) (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1 + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
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 ℕ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2)) =
    (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 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

Premises used: Polynomial.Chebyshev.U, Polynomial.degree, Nat.cast, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
succ :
  ∀ (m : ℕ) (hn : Ne (α := ℤ) (-(↑(m + 1) : ℤ)) (-1)),
    degree (U R (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 2)) =
      (↑((HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1).natAbs - 1) : WithBot ℕ)
⊢ degree (U R (HSub.hSub (α := ℤ) (↑m : ℤ) 2)) = (↑((HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 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

Premises used: Polynomial.Chebyshev.U, Polynomial.degree, Nat.cast, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
case₁ case₂ 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 ℕ)

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

Premises used: Polynomial.Chebyshev.U, Polynomial.degree, Nat.cast, Polynomial.Chebyshev.U_neg, Polynomial.degree_neg, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
neg : ¬n = -1 → natDegree (U R n) = (n + 1).natAbs - 1
⊢ natDegree (U R n) = (n + 1).natAbs - 1

Tactic:
by_cases n = -1
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
hn : n = -1
subst : natDegree (U R (-1)) = (HAdd.hAdd (α := ℤ) (-1) 1).natAbs - 1
⊢ natDegree (U R n) = (n + 1).natAbs - 1

Tactic:
subst hn
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ natDegree (U R (-1)) = (HAdd.hAdd (α := ℤ) (-1) 1).natAbs - 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℤ
h : n = -1
⊢ natDegree (U R n) = (n + 1).natAbs - 1

Tactic:
case pos hn => subst hn; simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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

Tactic:
natDegree_eq_of_degree_eq_some (degree_U_of_ne_neg_one R n hn)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.Chebyshev.degree_U_of_ne_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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

Tactic:
exact natDegree_eq_of_degree_eq_some (degree_U_of_ne_neg_one R n hn)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.Chebyshev.degree_U_of_ne_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 2 2
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff 2) 2

Tactic:
rw [← C_ofNat, leadingCoeff_C]

Premises used: Polynomial.C_ofNat, Polynomial.leadingCoeff_C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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

Tactic:
have : leadingCoeff (2 : R[X]) = 2 := by
    rw [← C_ofNat, leadingCoeff_C]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
⊢ leadingCoeff (U R (↑0 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
⊢ leadingCoeff (U R (↑1 : ℤ)) = HPow.hPow (α := R) (β := ℕ) 2 1

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ) 1)) = HPow.hPow (α := R) 2 (n + 1)

Tactic:
push_cast at ih2
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
more₁ : degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
⊢ leadingCoeff (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HPow.hPow (α := R) 2 (n + 2)

Tactic:
rw [U_add_two, leadingCoeff_sub_of_degree_lt, leadingCoeff_mul, ih2,
      leadingCoeff_mul, leadingCoeff_X, this]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_X, Polynomial.leadingCoeff_sub_of_degree_lt, Polynomial.Chebyshev.U_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 :
  Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 (n + 2)) : R)
⊢ HMul.hMul (α := R) 2 1 * HPow.hPow (α := R) 2 (n + 1) = HPow.hPow (α := R) 2 (n + 2)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 :
  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)
⊢ Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 1 * HPow.hPow (α := ℕ) 2 (n + 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 (n + 2)) : R)

Tactic:
rw [pow_add, pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 * HPow.hPow (α := ℕ) (β := ℕ) 2 1)) : R)
    (↑(HPow.hPow (α := ℕ) 2 n * HPow.hPow (α := ℕ) (β := ℕ) 2 2) : R)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : (↑n : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑(n + 1) : WithBot ℕ) 1
⊢ degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (↑(n + 1) : ℤ)).degree

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)]

Premises used: mul_assoc, two_ne_zero, HAdd.hAdd, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X, OfNat.ofNat, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : n < n + 1 + 1
⊢ (↑n : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑(n + 1) : WithBot ℕ) 1

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 < n + 1 + 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
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)
⊢ leadingCoeff (U R (↑n : ℤ)) = HPow.hPow (α := R) 2 n

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

Premises used: Polynomial.leadingCoeff_mul, mul_assoc, pow_add, Polynomial.leadingCoeff_X, Polynomial.leadingCoeff_sub_of_degree_lt, Polynomial.Chebyshev.U_add_two, two_ne_zero, HAdd.hAdd, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X, OfNat.ofNat, Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ eval (-x) (U R (↑0 : ℤ)) = (↑(↑(Int.negOnePow (↑0 : ℤ)) : ℤ) : R) * eval x (U R (↑0 : ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ eval (-x) (U R (↑1 : ℤ)) = (↑(↑(Int.negOnePow (↑1 : ℤ)) : ℤ) : R) * eval x (U R (↑1 : ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ)))
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) : ℤ))
⊢ eval (-x) (U R (↑(n + 2) : ℤ)) = (↑(↑(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)

Premises used: Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.U, HSub.hSub, Nat.cast, HAdd.hAdd, OfNat.ofNat, Int.negOnePow
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) * eval x (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))

Tactic:
push_cast at ih2
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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 : ℤ)))
⊢ 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 : ℤ)))

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]

Premises used: even_two, Int.negOnePow_add, Polynomial.eval_mul, Polynomial.Chebyshev.U_add_two, Int.negOnePow_even, OfNat.ofNat, Polynomial.eval_sub, Int.negOnePow_succ
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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 : ℤ)))
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
⊢ 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:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
⊢ (↑(↑(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:
simp