awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ 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
have 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
Tactic: cases n
Cleared hypotheses: n, p
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Bernstein (goal)
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
⊢ 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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
have refine : ∀ (n : ℕ), motive (-(↑n : ℤ)) → motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) → motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: refine Chebyshev.induct motive zero one add_two ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
have h₁ : n = - -n
Tactic: convert! neg (-n) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ n = - -n
have h₁ : n = n
Tactic: rw [neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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 : ℕ), motive (-(↑n : ℤ)) → motive (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) → motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg' : ∀ (n : ℤ) (h : motive (-n)), motive n
Tactic: have neg' (n : ℤ) (h : motive (-n)) : motive n := by
    convert! neg (-n) h; rw [neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 (HSub.hSub (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
have apply : motive (-(↑n : ℤ))
Tactic: apply neg (n + 2) (add_two n (neg' _ h₀) (neg' n ?_))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 (-(↑n : ℤ))
have h : -(↑n : ℤ) = HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1
Tactic: convert! h₁ using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have zero₁ : ∀ (h₀ : motive (-(↑0 : ℤ))) (h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)), motive (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 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
Cleared hypotheses: n, h₀, h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ motive (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have succ : ∀ (n : ℕ) (h₀ : motive (-(↑(n + 1) : ℤ))) (h₁ : motive (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)),
  motive (HSub.hSub (α := ℤ) (-(↑(n + 1) : ℤ)) 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
Cleared hypotheses: n, h₀, h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ 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
have 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
Tactic: simp [Int.negSucc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1) - T R (-(↑(k + 1) : ℤ))
have 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
Tactic: linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) T.eq_4 R k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n + 1) = HMul.hMul (α := R[X]) 2 X * T R n - T R (n - 1)
have 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
Tactic: linear_combination (norm := ring_nf) T_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n - 2) = HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R n
have 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
Tactic: linear_combination (norm := ring_nf) T_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n - 1) = HMul.hMul (α := R[X]) 2 X * T R n - T R (n + 1)
have 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
Tactic: linear_combination (norm := ring_nf) T_add_two R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R n = HMul.hMul (α := R[X]) 2 X * T R (n - 1) - T R (n - 2)
have 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
Tactic: linear_combination (norm := ring_nf) T_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (T R (Int.negSucc 0)) X
have rw : HMul.hMul (α := R[X]) 2 X * T R (-(↑0 : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
Tactic: rw [T]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) 2 X * T R (-(↑0 : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
have suffices : HMul.hMul (α := R[X]) 2 X - X = X
Tactic: suffices 2 * X - X = X by simpa
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ T R 2 = 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
have unfold : HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) - T R (↑0 : ℤ) =
  2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
Tactic: unfold T
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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 : ℤ))
⊢ Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have h₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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 : ℤ)
⊢ Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have h₂ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ))
⊢ Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have 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
Tactic: linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have h₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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)
⊢ Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have h₂ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
h₂ :
  T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have a : T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
      (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) + 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)) -
    (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
      (HMul.hMul (α := R[X]) 2 X * T R (- -(↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
          T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (T R (-n)) (T R n)
have zero : Eq (α := R[X]) (T R (-0)) (T R 0)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [T_neg_one, T_one]
  | add_two n ih1 ih2 =>
    have h₁ := T_add_two R n
    have h₂ := T_sub_two R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := T_add_one R n
    have h₂ := T_sub_one R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (T R (-0)) (T R 0)
⊢ Eq (α := R[X]) (T R (-n)) (T R n)
have one : Eq (α := R[X]) (T R (-1)) (T R 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [T_neg_one, T_one]
  | add_two n ih1 ih2 =>
    have h₁ := T_add_two R n
    have h₂ := T_sub_two R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := T_add_one R n
    have h₂ := T_sub_one R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (T R (-0)) (T R 0)
one : Eq (α := R[X]) (T R (-1)) (T R 1)
⊢ Eq (α := R[X]) (T R (-n)) (T R n)
have add_two : ∀ (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 : ℤ))),
  Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [T_neg_one, T_one]
  | add_two n ih1 ih2 =>
    have h₁ := T_add_two R n
    have h₂ := T_sub_two R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := T_add_one R n
    have h₂ := T_sub_one R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (T R (-0)) (T R 0)
one : Eq (α := R[X]) (T R (-1)) (T R 1)
add_two :
  ∀ (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 : ℤ))),
    Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
⊢ Eq (α := R[X]) (T R (-n)) (T R n)
have neg_add_one : ∀ (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))),
  Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [T_neg_one, T_one]
  | add_two n ih1 ih2 =>
    have h₁ := T_add_two R n
    have h₂ := T_sub_two R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := T_add_one R n
    have h₂ := T_sub_one R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
have inl : ∀ (h : n = (↑n.natAbs : ℤ)), Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
Tactic: obtain h | h := Int.natAbs_eq n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inl : ∀ (h : n = (↑n.natAbs : ℤ)), Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
have inr : ∀ (h : n = -(↑n.natAbs : ℤ)), Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
Tactic: obtain h | h := Int.natAbs_eq n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = (↑n.natAbs : ℤ)
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
have inl : Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R (↑n.natAbs : ℤ))
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = -(↑n.natAbs : ℤ)
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
have inr : Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R (-(↑n.natAbs : ℤ)))
Tactic: nth_rw 2 [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 1
ih2 : eval 1 (T R (↑n : ℤ)) = 1
⊢ eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 1
have add_two : HSub.hSub (α := R) 2 1 = 1
Tactic: simp [T_add_two, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (-(↑n : ℤ))) = 1
ih2 : eval 1 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 1
⊢ eval 1 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 1
have neg_add_one : HSub.hSub (α := R) 2 1 = 1
Tactic: simp [T_sub_one, -T_neg, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 1 (T R n) = 1
have zero : eval 1 (T R 0) = 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 1 (T R 0) = 1
⊢ eval 1 (T R n) = 1
have one : eval 1 (T R 1) = 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num
Cleared hypotheses: n