awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * n) : R[X]) X) * (↑x : R[X]) +
          (↑(HPow.hPow (β := ℕ) n 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
        bernsteinPolynomial R n x =
    (↑(n * (n - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * n) X) * HSMul.hSMul (β := R[X]) n X +
      HPow.hPow (β := ℕ) n 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
calc_2 :
  ∀
    (p :
      ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
          ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(HMul.hMul (α := ℕ) 2 0) : R[X]) X) * (↑x : R[X]) +
              (↑(HPow.hPow (α := ℕ) (β := ℕ) 0 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
            bernsteinPolynomial R 0 x =
        (↑(0 * HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            (1 - HSMul.hSMul (β := R[X]) (HMul.hMul (α := ℕ) 2 0) X) * HSMul.hSMul (α := ℕ) (β := R[X]) 0 X +
          HPow.hPow (α := ℕ) (β := ℕ) 0 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1),
    HMul.hMul (α := R[X]) (↑0 : R[X]) (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (1 - HMul.hMul (α := R[X]) 2 (↑0 : R[X]) * X) * HMul.hMul (α := R[X]) (↑0 : R[X]) X +
        HPow.hPow (α := R[X]) (β := ℕ) (↑0 : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
      HMul.hMul (α := R[X]) (↑0 : R[X]) X * HSub.hSub (α := R[X]) 1 X
calc_2₁ :
  ∀ (n : ℕ)
    (p :
      ∑ x ∈ Finset.range (n + 1 + 1),
          ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * (n + 1)) : R[X]) X) * (↑x : R[X]) +
              (↑(HPow.hPow (β := ℕ) (n + 1) 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
            bernsteinPolynomial R (n + 1) x =
        (↑((n + 1) * (n + 1 - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            (1 - HSMul.hSMul (β := R[X]) (2 * (n + 1)) X) * HSMul.hSMul (β := R[X]) (n + 1) X +
          HPow.hPow (β := ℕ) (n + 1) 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1),
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n + 1 - 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (1 - HMul.hMul (α := R[X]) 2 (↑(n + 1) : R[X]) * X) * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) X +
        HPow.hPow (α := R[X]) (β := ℕ) (↑(n + 1) : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
      HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) X * HSub.hSub (α := R[X]) 1 X
⊢ HMul.hMul (α := R[X]) (↑n : R[X]) (↑(n - 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HMul.hMul (α := R[X]) 2 (↑n : R[X]) * X) * HMul.hMul (α := R[X]) (↑n : R[X]) X +
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HMul.hMul (α := R[X]) (↑n : R[X]) X * HSub.hSub (α := R[X]) 1 X

Tactic:
cases n
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
p :
  ∑ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
      ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(HMul.hMul (α := ℕ) 2 0) : R[X]) X) * (↑x : R[X]) +
          (↑(HPow.hPow (α := ℕ) (β := ℕ) 0 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
        bernsteinPolynomial R 0 x =
    (↑(0 * HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (HMul.hMul (α := ℕ) 2 0) X) * HSMul.hSMul (α := ℕ) (β := R[X]) 0 X +
      HPow.hPow (α := ℕ) (β := ℕ) 0 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
⊢ HMul.hMul (α := R[X]) (↑0 : R[X]) (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HMul.hMul (α := R[X]) 2 (↑0 : R[X]) * X) * HMul.hMul (α := R[X]) (↑0 : R[X]) X +
      HPow.hPow (α := R[X]) (β := ℕ) (↑0 : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HMul.hMul (α := R[X]) (↑0 : R[X]) X * HSub.hSub (α := R[X]) 1 X

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1 + 1),
      ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * (n + 1)) : R[X]) X) * (↑x : R[X]) +
          (↑(HPow.hPow (β := ℕ) (n + 1) 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
        bernsteinPolynomial R (n + 1) x =
    (↑((n + 1) * (n + 1 - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * (n + 1)) X) * HSMul.hSMul (β := R[X]) (n + 1) X +
      HPow.hPow (β := ℕ) (n + 1) 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
calc_2 :
  HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - 2 * HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X) * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X) +
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X * HSub.hSub (α := R[X]) 1 X
⊢ HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (↑(n + 1 - 1) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HMul.hMul (α := R[X]) 2 (↑(n + 1) : R[X]) * X) * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) X +
      HPow.hPow (α := R[X]) (β := ℕ) (↑(n + 1) : R[X]) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1 =
    HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) X * HSub.hSub (α := R[X]) 1 X

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Bernstein
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1 + 1),
      ((↑(x * (x - 1)) : R[X]) + (1 - HMul.hMul (α := R[X]) (↑(2 * (n + 1)) : R[X]) X) * (↑x : R[X]) +
          (↑(HPow.hPow (β := ℕ) (n + 1) 2) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2) *
        bernsteinPolynomial R (n + 1) x =
    (↑((n + 1) * (n + 1 - 1)) : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - HSMul.hSMul (β := R[X]) (2 * (n + 1)) X) * HSMul.hSMul (β := R[X]) (n + 1) X +
      HPow.hPow (β := ℕ) (n + 1) 2 • HPow.hPow (α := R[X]) (β := ℕ) X 2 * 1
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (1 - 2 * HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X) * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X) +
      HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * X * HSub.hSub (α := R[X]) 1 X

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg_add_one :
  ∀ (n : ℕ), motive (-(↑n : ℤ)) → motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) → motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
n : ℕ
hn : motive (-(↑n : ℤ))
hnm : motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ motive (Int.negSucc n)

Tactic:
simpa only [Int.negSucc_eq, neg_add] using neg_add_one n hn hnm

Premises used: neg_add, Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (a : ℤ), motive a

Tactic:
Chebyshev.induct motive zero one add_two ?_

Premises used: Polynomial.Chebyshev.induct
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
refine :
  ∀ (n : ℕ), motive (-(↑n : ℤ)) → motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) → motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ ∀ (a : ℤ), motive a

Tactic:
refine Chebyshev.induct motive zero one add_two ?_

Premises used: Polynomial.Chebyshev.induct
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
n : ℤ
h : motive (-n)
⊢ motive (- -n)

Tactic:
neg (-n) h

Premises used: Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
n : ℤ
h : motive (-n)
h₁ : n = - -n
⊢ motive n

Tactic:
convert! neg (-n) h

Premises used: Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
n : ℤ
h : motive (-n)
h₁ h₂ : n = n
⊢ n = - -n

Tactic:
rw [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
⊢ ∀ (n : ℤ) (h : motive (-n)), motive n

Tactic:
have neg' (n : ℤ) (h : motive (-n)) : motive n := by
    convert! neg (-n) h; rw [neg_neg]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
h₀ : motive (-(↑0 : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)
⊢ motive (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1)

Tactic:
neg 1 h₁

Premises used: Int.sub, Int.subNatNat, OfNat.ofNat, Int.add, Int.neg, Int.negOfNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
h₀ : motive (-(↑0 : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)
⊢ motive (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1)

Tactic:
exact neg 1 h₁

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
n : ℕ
h₀ : motive (-(↑(n + 1) : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
apply : motive (-(↑n : ℤ))
⊢ motive (HSub.hSub (α := ℤ) (-(↑(n + 1) : ℤ)) 1)

Tactic:
apply neg (n + 2) (add_two n (neg' _ h₀) (neg' n ?_))

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
n : ℕ
h₀ : motive (-(↑(n + 1) : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
⊢ motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)

Tactic:
h₁
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
n : ℕ
h₀ : motive (-(↑(n + 1) : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
h : -(↑n : ℤ) = HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1
⊢ motive (-(↑n : ℤ))

Tactic:
convert! h₁ using 1
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
n : ℕ
h₀ : motive (-(↑(n + 1) : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
⊢ -(↑n : ℤ) = HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1

Tactic:
omega
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
motive : ℤ → Prop
zero : motive 0
one : motive 1
add_two : ∀ (n : ℕ), motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) → motive (↑n : ℤ) → motive (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg : ∀ (n : ℤ), motive n → motive (-n)
neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
n : ℕ
h₀ : motive (-(↑n : ℤ))
h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
zero₁ :
  ∀ (h₀ : motive (-(↑0 : ℤ))) (h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)),
    motive (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1)
succ :
  ∀ (n : ℕ) (h₀ : motive (-(↑(n + 1) : ℤ))) (h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)),
    motive (HSub.hSub (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
⊢ motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
cases n with
  | zero => exact neg 1 h₁
  | succ n =>
    apply neg (n + 2) (add_two n (neg' _ h₀) (neg' n ?_))
    convert! h₁ using 1; omega
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a :
  T R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) =
    0
⊢ T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - T R (-(↑(k + 1) : ℤ)) +
        T R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Premises used: Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ T R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a :
  T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑k : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - T R (-(↑(k + 1) : ℤ)) +
        T R (Int.negSucc k)) =
    0
⊢ T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - T R (-(↑(k + 1) : ℤ))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) T.eq_4 R k

Premises used: Polynomial.Chebyshev.T.eq_4, Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n + 1) + (HMul.hMul (α := R[X]) 2 X * T R (n - 1 + 1) - T R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R n - T R (n - 1) + T R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  T R (n + 1) + (HMul.hMul (α := R[X]) 2 X * T R (n - 1 + 1) - T R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R n - T R (n - 1) + T R (n - 1 + 2)) =
    0
⊢ T R (n + 1) = HMul.hMul (α := R[X]) 2 X * T R n - T R (n - 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.T_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n - 2) + (HMul.hMul (α := R[X]) 2 X * T R (n - 2 + 1) - T R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R n + T R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  T R (n - 2) + (HMul.hMul (α := R[X]) 2 X * T R (n - 2 + 1) - T R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R n + T R (n - 2 + 2)) =
    0
⊢ T R (n - 2) = HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R n

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.T_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n - 1) + (HMul.hMul (α := R[X]) 2 X * T R (n - 1 + 1) - T R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R n - T R (n + 1) + T R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  T R (n - 1) + (HMul.hMul (α := R[X]) 2 X * T R (n - 1 + 1) - T R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * T R n - T R (n + 1) + T R (n - 1 + 2)) =
    0
⊢ T R (n - 1) = HMul.hMul (α := R[X]) 2 X * T R n - T R (n + 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.T_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R n + (HMul.hMul (α := R[X]) 2 X * T R (n - 2 + 1) - T R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R (n - 2) + T R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  T R n + (HMul.hMul (α := R[X]) 2 X * T R (n - 2 + 1) - T R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R (n - 2) + T R (n - 2 + 2)) =
    0
⊢ T R n = HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R (n - 2)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.T_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (T R 0) 1

Tactic:
simp [T]

Premises used: Polynomial.Chebyshev.T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (T R 1) X

Tactic:
simp [T]

Premises used: Polynomial.Chebyshev.T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
rw : HMul.hMul (α := R[X]) 2 X * T R (-(↑0 : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
⊢ Eq (α := R[X]) (T R (Int.negSucc 0)) X

Tactic:
rw [T]

Premises used: Polynomial.Chebyshev.T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : HMul.hMul (α := R[X]) 2 X - X = X
⊢ HMul.hMul (α := R[X]) 2 X * T R (-(↑0 : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
suffices : HMul.hMul (α := R[X]) 2 X - X = X
⊢ HMul.hMul (α := R[X]) 2 X * T R (-(↑0 : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X

Tactic:
suffices 2 * X - X = X by simpa
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) 2 X - X = X

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
unfold :
  HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) - T R (↑0 : ℤ) =
    2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
⊢ T R 2 = 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1

Tactic:
unfold T

Premises used: Polynomial.Chebyshev.T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) - T R (↑0 : ℤ) =
    2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1

Tactic:
simp [pow_two, mul_assoc]

Premises used: pow_two, mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (T R (-0)) (T R 0)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (T R (-1)) (T R 1)

Tactic:
simp only [T_neg_one, T_one]

Premises used: Polynomial.Chebyshev.T_one, Polynomial.Chebyshev.T_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (T R (-(↑n : ℤ))) (T R (↑n : ℤ))
⊢ T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)

Tactic:
have h₁ := T_add_two R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (T R (-(↑n : ℤ))) (T R (↑n : ℤ))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)
⊢ T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ))

Tactic:
have h₂ := T_sub_two R (-n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (T R (-(↑n : ℤ))) (T R (↑n : ℤ))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)
h₂ :
  T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ))
⊢ T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + T R (-(↑n : ℤ)) +
            T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
          (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ)))) -
      (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + T R (↑n : ℤ) +
            (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) +
          T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (T R (-(↑n : ℤ))) (T R (↑n : ℤ))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)
h₂ :
  T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ))
a :
  T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + T R (-(↑n : ℤ)) +
            T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
          (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ)))) -
      (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 X * T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + T R (↑n : ℤ) +
            (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) +
          T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
    0
⊢ Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂

Premises used: HMul.hMul, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (- -(↑n : ℤ))) (T R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
⊢ T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)

Tactic:
have h₁ := T_add_one R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (- -(↑n : ℤ))) (T R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
⊢ T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
have h₂ := T_sub_one R (-n)