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
n : ℕ
x : R
⊢ eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
have zero : eval (-x) (U R (↑0 : ℤ)) = (↑(↑(Int.negOnePow (↑0 : ℤ)) : ℤ) : R) * eval x (U R (↑0 : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
    · push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring
    · simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : R
zero : eval (-x) (U R (↑0 : ℤ)) = (↑(↑(Int.negOnePow (↑0 : ℤ)) : ℤ) : R) * eval x (U R (↑0 : ℤ))
⊢ eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
have one : eval (-x) (U R (↑1 : ℤ)) = (↑(↑(Int.negOnePow (↑1 : ℤ)) : ℤ) : R) * eval x (U R (↑1 : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
    · push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring
    · simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : R
zero : eval (-x) (U R (↑0 : ℤ)) = (↑(↑(Int.negOnePow (↑0 : ℤ)) : ℤ) : R) * eval x (U R (↑0 : ℤ))
one : eval (-x) (U R (↑1 : ℤ)) = (↑(↑(Int.negOnePow (↑1 : ℤ)) : ℤ) : R) * eval x (U R (↑1 : ℤ))
⊢ eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))
have more : ∀ (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) : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
    · push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring
    · simp
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
h : Eq (α := R[X]) (U R n) 0
⊢ n = -1
have contrapose! : ∀ (h : n ≠ -1), Ne (α := R[X]) (U R n) 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ U R (HAdd.hAdd (α := ℤ) 1 1) = HMul.hMul (α := R[X]) X (U R 1) + T R (HAdd.hAdd (α := ℤ) 1 1)
have one : 4 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1 =
  X * HMul.hMul (α := R[X]) 2 X + (2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1)
Tactic: simp [U_two, T_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₁ : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₁ := U_add_two R (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₂ : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: have h₂ := U_add_two R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₂ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₃ : T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
  HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₃ := 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 : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₂ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have a : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) +
      (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) + HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) +
            (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) -
              U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
          HMul.hMul (α := R[X]) 2 X *
            (HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
        U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
    (HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) +
      (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
              X * (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) +
            U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) +
          HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) +
        (HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
⊢ U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have h₁ : U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₁ := U_add_two R (-n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have h₂ : U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
Tactic: have h₂ := U_add_two R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
h₂ :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
⊢ U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
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 (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
h₂ :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
h₃ :
  T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ))
⊢ U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have a : U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
      (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) +
              (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))) +
            HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2)) +
          U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
        HMul.hMul (α := R[X]) 2 X *
          (HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))) -
    (HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
      (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - T R (-(↑n : ℤ)) +
              U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) +
            X *
              (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) -
                U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) +
          (HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
            T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
        HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))) =
  0
Tactic: linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
have zero : U R (HAdd.hAdd (α := ℤ) 0 1) = HMul.hMul (α := R[X]) X (U R 0) + T R (HAdd.hAdd (α := ℤ) 0 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : U R (HAdd.hAdd (α := ℤ) 0 1) = HMul.hMul (α := R[X]) X (U R 0) + T R (HAdd.hAdd (α := ℤ) 0 1)
⊢ U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
have one : U R (HAdd.hAdd (α := ℤ) 1 1) = HMul.hMul (α := R[X]) X (U R 1) + T R (HAdd.hAdd (α := ℤ) 1 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : U R (HAdd.hAdd (α := ℤ) 0 1) = HMul.hMul (α := R[X]) X (U R 0) + T R (HAdd.hAdd (α := ℤ) 0 1)
one : U R (HAdd.hAdd (α := ℤ) 1 1) = HMul.hMul (α := R[X]) X (U R 1) + T R (HAdd.hAdd (α := ℤ) 1 1)
⊢ U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
have add_two : ∀ (n : ℕ)
  (ih1 :
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
      HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1))
  (ih2 :
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)),
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : U R (HAdd.hAdd (α := ℤ) 0 1) = HMul.hMul (α := R[X]) X (U R 0) + T R (HAdd.hAdd (α := ℤ) 0 1)
one : U R (HAdd.hAdd (α := ℤ) 1 1) = HMul.hMul (α := R[X]) X (U R 1) + T R (HAdd.hAdd (α := ℤ) 1 1)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
        HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1))
    (ih2 :
      U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
        HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)),
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) =
      HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
⊢ U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
have neg_add_one : ∀ (n : ℕ)
  (ih1 :
    U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
      HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
  (ih2 :
    U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
      HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)),
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R n = U R n - HMul.hMul (α := R[X]) X (U R (n - 1))
have a : HAdd.hAdd (α := R[X]) (T R n) (U R (n - 1 + 1)) -
    (U R n - HMul.hMul (α := R[X]) X (U R (n - 1)) + (HMul.hMul (α := R[X]) X (U R (n - 1)) + T R (n - 1 + 1))) =
  0
Tactic: linear_combination (norm := ring_nf) - U_eq_X_mul_U_add_T R (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n
have h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
Tactic: have h₁ := U_eq_X_mul_U_add_T R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n
have h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
Tactic: have h₂ := U_eq_X_mul_U_add_T R (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n
have h₃ : U R (n + 2) = HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n
Tactic: have h₃ := U_add_two R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
h₃ : U R (n + 2) = HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n
have a : T R (n + 2) +
      (HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n + U R (n + 1 + 1) +
        X * (HMul.hMul (α := R[X]) X (U R n) + T R (n + 1))) -
    (HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n +
      (U R (n + 2) + (HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)) +
        HMul.hMul (α := R[X]) X (U R (n + 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) h₃ - h₂ + (X : R[X]) * h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n
have h : T R (-(n + 2)) = U R (-(n + 2)) - HMul.hMul (α := R[X]) X (U R (-(n + 2) - 1))
Tactic: have h := T_eq_U_sub_X_mul_U (R := R) (-(n + 2))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (-(n + 2)) = U R (-(n + 2)) - HMul.hMul (α := R[X]) X (U R (-(n + 2) - 1))
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n
have h₁ : T R (n + 2) = -U R n - HMul.hMul (α := R[X]) X (-U R (n + 1))
Tactic: rw [T_neg, U_neg, Int.add_sub_cancel, ← neg_add' _ 1, U_neg,
    show n + 2 + 1 - 2 = n + 1 by ring] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n + 2) = -U R n - HMul.hMul (α := R[X]) X (-U R (n + 1))
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n
have a : T R (n + 2) + (-U R n - HMul.hMul (α := R[X]) X (-U R (n + 1))) -
    (HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n + T R (n + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R (n + 2)) = HSub.hSub (α := R[X]) (U R (n + 2)) (U R n)
have a : HMul.hMul (α := R[X]) 2 (T R (n + 2)) +
      (U R (n + 2) - HMul.hMul (α := R[X]) X (U R (n + 2 - 1)) + (HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n)) -
    (HSub.hSub (α := R[X]) (U R (n + 2)) (U R n) + HAdd.hAdd (α := R[X]) (T R (n + 2)) (T R (n + 2))) =
  0
Tactic: linear_combination (norm := ring_nf) (T_eq_U_sub_X_mul_U R (n + 2)) + (T_eq_X_mul_U_sub_U R n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n + 2) = HMul.hMul (α := R[X]) 2 (T R (n + 2)) + U R n
have a : U R (n + 2) + HMul.hMul (α := R[X]) 2 (T R (n + 2)) -
    (HMul.hMul (α := R[X]) 2 (T R (n + 2)) + U R n + HSub.hSub (α := R[X]) (U R (n + 2)) (U R n)) =
  0
Tactic: linear_combination (norm := ring_nf) - (two_mul_T_eq_U_sub_U R n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1)) (U R (↑1 : ℤ))
have one : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1))
  (HSMul.hSMul (α := R[X]) (β := R[X]) 2 (T R 1))
Tactic: rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1))
    (HSMul.hSMul (α := R[X]) (β := R[X]) 2 (T R 1))
have one : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1))
  (HSMul.hSMul (α := ℕ) (β := R[X]) 2 (T R 1))
Tactic: norm_cast