awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
          𝔽) *
        HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 /
      (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽)
have rw : eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) =
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : 𝔽) *
    HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_U_eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
          𝔽) *
        HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 /
      (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽)
have rw₁ : (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : 𝔽) *
    HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_U_eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
rw₁ :
  (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
          𝔽) *
        HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 /
      (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽)
have rw₂ : (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : 𝔽) *
    HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 =
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : 𝔽) *
    HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_U_eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))
have one : HMul.hMul (α := R[X]) 2 (T R m) * X = HMul.hMul (α := R[X]) 2 X * T R m - T R (m - 1) + T R (m - 1)
Tactic: rw [T_add_one, T_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
Tactic: have h₁ := T_add_two R (m + k)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
Tactic: have h₂ := T_sub_two R (m - k)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₃ : T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)
Tactic: have h₃ := T_add_two R k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have a : HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
      (HMul.hMul (α := R[X]) 2 (T R m) *
                (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)) +
              T R (m - (↑k : ℤ) - 2) +
            T R (m + (↑k : ℤ) + 2) +
          HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) +
        HMul.hMul (α := R[X]) 2 X *
          HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))) -
    (HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) +
      (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
              (HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))) +
            (HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))) +
          HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ))) +
        HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
have h₁ : T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
  HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
    T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
Tactic: have h₁ := T_add_two R (m + (-k - 1))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
have h₂ : T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
  HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
    T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
Tactic: have h₂ := T_sub_two R (m - (-k - 1))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₂ :
  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
have h₃ : T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
  HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
Tactic: have h₃ := T_add_two R (-k - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₂ :
  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₃ :
  T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
have a : HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) +
      (HMul.hMul (α := R[X]) 2 (T R m) *
                (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
                  T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
              T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) +
            T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
          HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) +
        HMul.hMul (α := R[X]) 2 X * HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))) -
    (HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
      (HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
              (HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
                T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
            (HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
              T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
          HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
            (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) +
        HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ))))) =
  0
Tactic: linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - 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
m k : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R k = HAdd.hAdd (α := R[X]) (T R (m + k)) (T R (m - k))
have zero : HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))
Tactic: induction k using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => rw [T_add_one, T_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := T_add_two R (m + k)
    have h₂ := T_sub_two R (m - k)
    have h₃ := T_add_two R k
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m k : ℤ
zero : HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R k = HAdd.hAdd (α := R[X]) (T R (m + k)) (T R (m - k))
have one : HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))
Tactic: induction k using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => rw [T_add_one, T_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := T_add_two R (m + k)
    have h₂ := T_sub_two R (m - k)
    have h₃ := T_add_two R k
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m k : ℤ
zero : HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))
one : HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R k = HAdd.hAdd (α := R[X]) (T R (m + k)) (T R (m - k))
have add_two : ∀ (k : ℕ)
  (ih1 :
    HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
      HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))
  (ih2 :
    HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))),
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
Tactic: induction k using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => rw [T_add_one, T_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := T_add_two R (m + k)
    have h₂ := T_sub_two R (m - k)
    have h₃ := T_add_two R k
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m k : ℤ
zero : HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))
one : HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))
add_two :
  ∀ (k : ℕ)
    (ih1 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
        HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))
    (ih2 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))),
    HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
      HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R k = HAdd.hAdd (α := R[X]) (T R (m + k)) (T R (m - k))
have neg_add_one : ∀ (k : ℕ)
  (ih1 :
    HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) =
      HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ))))
  (ih2 :
    HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
      HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))),
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
Tactic: induction k using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => rw [T_add_one, T_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := T_add_two R (m + k)
    have h₂ := T_sub_two R (m - k)
    have h₃ := T_add_two R k
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) (C R m) (C R 1) = HAdd.hAdd (α := R[X]) (C R (m + 1)) (C R (m - 1))
have one : HMul.hMul (α := R[X]) (C R m) X = HMul.hMul (α := R[X]) X (C R m) - C R (m - 1) + C R (m - 1)
Tactic: rw [C_add_one, C_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) (C R m) (C R (↑k : ℤ)) = HAdd.hAdd (α := R[X]) (C R (m + (↑k : ℤ))) (C R (m - (↑k : ℤ)))
⊢ HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₁ : C R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) X (C R (m + (↑k : ℤ) + 1)) - C R (m + (↑k : ℤ))
Tactic: have h₁ := C_add_two R (m + k)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) (C R m) (C R (↑k : ℤ)) = HAdd.hAdd (α := R[X]) (C R (m + (↑k : ℤ))) (C R (m - (↑k : ℤ)))
h₁ : C R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) X (C R (m + (↑k : ℤ) + 1)) - C R (m + (↑k : ℤ))
⊢ HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₂ : C R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) X (C R (m - (↑k : ℤ) - 1)) - C R (m - (↑k : ℤ))
Tactic: have h₂ := C_sub_two R (m - k)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) (C R m) (C R (↑k : ℤ)) = HAdd.hAdd (α := R[X]) (C R (m + (↑k : ℤ))) (C R (m - (↑k : ℤ)))
h₁ : C R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) X (C R (m + (↑k : ℤ) + 1)) - C R (m + (↑k : ℤ))
h₂ : C R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) X (C R (m - (↑k : ℤ) - 1)) - C R (m - (↑k : ℤ))
⊢ HMul.hMul (α := R[X]) (C R m) (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have h₃ : C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) - C R (↑k : ℤ)
Tactic: have h₃ := C_add_two R k