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 : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    1
h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    1
have a : HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) +
      (HSub.hSub (α := R[X]) (S R (HAdd.hAdd (α := ℤ) 2 (↑n : ℤ))) (S R (↑n : ℤ)) *
          (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) +
        1) -
    (1 +
      (HSub.hSub (α := R[X]) (S R (HAdd.hAdd (α := ℤ) 2 (↑n : ℤ))) (S R (↑n : ℤ)) *
          S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    1
have h₁ : S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
  HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₁ := S_sub_one R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    1
h₁ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    1
have a : HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
      (HSub.hSub (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) (↑n : ℤ))) (S R (HSub.hSub (α := ℤ) 1 (↑n : ℤ))) *
          (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
        1) -
    (1 +
      (HSub.hSub (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) (↑n : ℤ))) (S R (HSub.hSub (α := ℤ) 1 (↑n : ℤ))) *
          S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
        (HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R n) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (n + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R n) * S R (n + 1) =
    1
have zero : HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
    HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
  1
Tactic: induction n with
  | zero => simp; ring
  | succ n ih =>
    have h₁ := S_add_two R n
    linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
  | pred n ih =>
    have h₁ := S_sub_one R (-n)
    linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero :
  HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
      HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
    1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R n) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (n + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R n) * S R (n + 1) =
    1
have succ : ∀ (n : ℕ)
  (ih :
    HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
      1),
  HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    1
Tactic: induction n with
  | zero => simp; ring
  | succ n ih =>
    have h₁ := S_add_two R n
    linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
  | pred n ih =>
    have h₁ := S_sub_one R (-n)
    linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero :
  HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
      HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
    1
succ :
  ∀ (n : ℕ)
    (ih :
      HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
        1),
    HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
      1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R n) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (n + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R n) * S R (n + 1) =
    1
have pred : ∀ (n : ℕ)
  (ih :
    HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
      1),
  HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    1
Tactic: induction n with
  | zero => simp; ring
  | succ n ih =>
    have h₁ := S_add_two R n
    linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
  | pred n ih =>
    have h₁ := S_sub_one R (-n)
    linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
⊢ S R n =
    comp (U R n)
      (HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)
have this : Eq.{u_1 + 1} (α := R[X])
  ((fun (x : R[X]) ↦
      x.comp
        (HMul.hMul (α := R[X])
          ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
    (comp (S R n) (HMul.hMul (α := R[X]) 2 X)))
  ((fun (x : R[X]) ↦
      x.comp
        (HMul.hMul (α := R[X])
          ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
    (U R n))
Tactic: have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (S_comp_two_mul_X R n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 1 1)) =
    HMul.hMul (α := R[X]) X (S R 1) + C R (HAdd.hAdd (α := ℤ) 1 1)
have one : 2 * (HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1) = HMul.hMul (α := R[X]) X X + (HPow.hPow (α := R[X]) (β := ℕ) X 2 - 2)
Tactic: simp [S_two, C_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
  HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₁ := S_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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₂ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
Tactic: have h₂ := S_add_two R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₂ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have h₃ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
  HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₃ := C_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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₁ :
  S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₂ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
h₃ :
  C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
have a : HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) +
      (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) + HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) +
            2 *
              (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) -
                S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
          X *
            (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
        HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
    (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) +
      (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
              X * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) +
            HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2)) +
          X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
        (HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have h₁ : S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
  HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₁ := S_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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have h₂ : S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
Tactic: have h₂ := S_add_two R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
h₂ :
  S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have h₃ : C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
Tactic: have h₃ := C_add_two R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)
h₁ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
h₂ :
  S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
h₃ :
  C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
have a : HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
      (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) +
              2 * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))) +
            HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2)) +
          HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
        X * (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))) -
    (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
      (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ)) +
              HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2)) +
            X *
              (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) -
                S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) +
          (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
            C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
        X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (X : R[X]) * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HMul.hMul (α := R[X]) 2 (S R (n + 1)) = HMul.hMul (α := R[X]) X (S R n) + C R (n + 1)
have zero : HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 0 1)) = HMul.hMul (α := R[X]) X (S R 0) + C R (HAdd.hAdd (α := ℤ) 0 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [S_two, C_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := S_add_two R (n + 1)
    have h₂ := S_add_two R n
    have h₃ := C_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_add_two R (-n - 1)
    have h₂ := S_add_two R (-n)
    have h₃ := C_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 0 1)) =
    HMul.hMul (α := R[X]) X (S R 0) + C R (HAdd.hAdd (α := ℤ) 0 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (n + 1)) = HMul.hMul (α := R[X]) X (S R n) + C R (n + 1)
have one : HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 1 1)) = HMul.hMul (α := R[X]) X (S R 1) + C R (HAdd.hAdd (α := ℤ) 1 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [S_two, C_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := S_add_two R (n + 1)
    have h₂ := S_add_two R n
    have h₃ := C_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_add_two R (-n - 1)
    have h₂ := S_add_two R (-n)
    have h₃ := C_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (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 :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 0 1)) =
    HMul.hMul (α := R[X]) X (S R 0) + C R (HAdd.hAdd (α := ℤ) 0 1)
one :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 1 1)) =
    HMul.hMul (α := R[X]) X (S R 1) + C R (HAdd.hAdd (α := ℤ) 1 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (n + 1)) = HMul.hMul (α := R[X]) X (S R n) + C R (n + 1)
have add_two : ∀ (n : ℕ)
  (ih1 :
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) =
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1))
  (ih2 :
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
      HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)),
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [S_two, C_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := S_add_two R (n + 1)
    have h₂ := S_add_two R n
    have h₃ := C_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + 2 * h₁ + (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_add_two R (-n - 1)
    have h₂ := S_add_two R (-n)
    have h₃ := C_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X : R[X]) * h₁ - ih2 + (X : R[X]) * ih1
Cleared hypotheses: n