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 : ℕ
h₀ :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
h :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 1)))
    (U R (↑(n + 1) : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
    (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have more : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
  (HSMul.hSMul (α := R[X]) (β := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + U R (↑n : ℤ))
Tactic: rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
h₀ :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
h :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 1)))
    (U R (↑(n + 1) : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
    (HSMul.hSMul (α := R[X]) (β := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + U R (↑n : ℤ))
have more : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
  (HSMul.hSMul (α := ℕ) (β := R[X]) 2 (T R (↑(n + 2) : ℤ)) + U R (↑n : ℤ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
h₀ :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
h :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 1)))
    (U R (↑(n + 1) : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
    (HSMul.hSMul (α := ℕ) (β := R[X]) 2 (T R (↑(n + 2) : ℤ)) + U R (↑n : ℤ))
have more : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
  (HSMul.hSMul (α := ℕ) (β := R[X]) 2 (T R (↑(n + 2) : ℤ)))
Tactic: refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
have zero : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 0)) (U R (↑0 : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]; norm_cast
    exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)
  | more n h₀ _ =>
    push_cast; rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]; norm_cast
    refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
    · exact Submodule.smul_of_tower_mem _ 2
        (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
zero :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 0)) (U R (↑0 : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
have one : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1)) (U R (↑1 : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]; norm_cast
    exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)
  | more n h₀ _ =>
    push_cast; rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]; norm_cast
    refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
    · exact Submodule.smul_of_tower_mem _ 2
        (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
zero :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 0)) (U R (↑0 : ℤ))
one :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1)) (U R (↑1 : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))
have more : ∀ (n : ℕ)
  (h₀ :
    Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n))
      (U R (↑n : ℤ))),
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 1)))
      (U R (↑(n + 1) : ℤ)) →
    Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
      (U R (↑(n + 2) : ℤ))
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]; norm_cast
    exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)
  | more n h₀ _ =>
    push_cast; rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]; norm_cast
    refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)
    · exact Submodule.smul_of_tower_mem _ 2
        (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
        (HMul.hMul (α := R[X]) X (C R (-(↑k : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
      (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - C R (-(↑(k + 1) : ℤ)) +
        C R (Int.negSucc k)) =
    0
have a : C R (HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)) + 2) +
      (HMul.hMul (α := R[X]) X (C R (-(↑k : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
    HMul.hMul (α := R[X]) X (C 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 : ℕ
⊢ C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - C R (-(↑(k + 1) : ℤ))
have a : C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) +
      (HMul.hMul (α := R[X]) X (C R (-(↑k : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) -
    (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - C R (-(↑(k + 1) : ℤ)) +
      C R (Int.negSucc k)) =
  0
Tactic: linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) C.eq_4 R k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ C R (n + 1) = HMul.hMul (α := R[X]) X (C R n) - C R (n - 1)
have a : C R (n + 1) + (HMul.hMul (α := R[X]) X (C R (n - 1 + 1)) - C R (n - 1)) -
    (HMul.hMul (α := R[X]) X (C R n) - C R (n - 1) + C R (n - 1 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) 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 : ℤ
⊢ C R (n - 2) = HMul.hMul (α := R[X]) X (C R (n - 1)) - C R n
have a : C R (n - 2) + (HMul.hMul (α := R[X]) X (C R (n - 2 + 1)) - C R (n - 2)) -
    (HMul.hMul (α := R[X]) X (C R (n - 1)) - C R n + C R (n - 2 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) C_add_two R (n - 2)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ C R (n - 1) = HMul.hMul (α := R[X]) X (C R n) - C R (n + 1)
have a : C R (n - 1) + (HMul.hMul (α := R[X]) X (C R (n - 1 + 1)) - C R (n - 1)) -
    (HMul.hMul (α := R[X]) X (C R n) - C R (n + 1) + C R (n - 1 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) 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 : ℤ
⊢ C R n = HMul.hMul (α := R[X]) X (C R (n - 1)) - C R (n - 2)
have a : C R n + (HMul.hMul (α := R[X]) X (C R (n - 2 + 1)) - C R (n - 2)) -
    (HMul.hMul (α := R[X]) X (C R (n - 1)) - C R (n - 2) + C R (n - 2 + 2)) =
  0
Tactic: linear_combination (norm := ring_nf) C_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]) (C R (Int.negSucc 0)) X
have rw : HMul.hMul (α := R[X]) X (C R (-(↑0 : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
Tactic: rw [C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) X (C R (-(↑0 : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
have suffices : HMul.hMul (α := R[X]) X 2 - X = X
Tactic: suffices X * 2 - X = X by simpa
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (C R (-(↑n : ℤ))) (C R (↑n : ℤ))
⊢ Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
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 (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (C R (-(↑n : ℤ))) (C R (↑n : ℤ))
h₁ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)
⊢ Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have h₂ : C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
Tactic: have h₂ := C_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]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : Eq (α := R[X]) (C R (-(↑n : ℤ))) (C R (↑n : ℤ))
h₁ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)
h₂ :
  C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
⊢ Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have a : C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
      (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (-(↑n : ℤ)) +
          C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
        (HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ)))) -
    (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
      (HMul.hMul (α := R[X]) X (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + C R (↑n : ℤ) +
          (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - C R (↑n : ℤ)) +
        C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
  0
Tactic: linear_combination (norm := ring_nf) (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]) (C R (- -(↑n : ℤ))) (C R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
⊢ Eq (α := R[X]) (C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have h₁ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (C R (↑n : ℤ)) - C R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₁ := C_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]) (C R (- -(↑n : ℤ))) (C R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
h₁ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (C R (↑n : ℤ)) - C R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
⊢ Eq (α := R[X]) (C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have h₂ : C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
  HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₂ := C_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]) (C R (- -(↑n : ℤ))) (C R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
h₁ : C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (C R (↑n : ℤ)) - C R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ Eq (α := R[X]) (C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have a : C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
      (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) + C R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
          (HMul.hMul (α := R[X]) X (C R (↑n : ℤ)) - C R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
        C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) -
    (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
      (HMul.hMul (α := R[X]) X (C R (- -(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
          C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        (HMul.hMul (α := R[X]) X (C R (-(↑n : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
  0
Tactic: linear_combination (norm := ring_nf) (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]) (C R (-n)) (C R n)
have zero : Eq (α := R[X]) (C R (-0)) (C R 0)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [C_neg_one, C_one]
  | add_two n ih1 ih2 =>
    have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := C_add_one R n
    have h₂ := C_sub_one R (-n)
    linear_combination (norm := ring_nf) (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]) (C R (-0)) (C R 0)
⊢ Eq (α := R[X]) (C R (-n)) (C R n)
have one : Eq (α := R[X]) (C R (-1)) (C R 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [C_neg_one, C_one]
  | add_two n ih1 ih2 =>
    have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := C_add_one R n
    have h₂ := C_sub_one R (-n)
    linear_combination (norm := ring_nf) (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]) (C R (-0)) (C R 0)
one : Eq (α := R[X]) (C R (-1)) (C R 1)
⊢ Eq (α := R[X]) (C R (-n)) (C R n)
have add_two : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
  (ih2 : Eq (α := R[X]) (C R (-(↑n : ℤ))) (C R (↑n : ℤ))),
  Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [C_neg_one, C_one]
  | add_two n ih1 ih2 =>
    have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := C_add_one R n
    have h₂ := C_sub_one R (-n)
    linear_combination (norm := ring_nf) (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]) (C R (-0)) (C R 0)
one : Eq (α := R[X]) (C R (-1)) (C R 1)
add_two :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
    (ih2 : Eq (α := R[X]) (C R (-(↑n : ℤ))) (C R (↑n : ℤ))),
    Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
⊢ Eq (α := R[X]) (C R (-n)) (C R n)
have neg_add_one : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (C R (- -(↑n : ℤ))) (C R (-(↑n : ℤ))))
  (ih2 : Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))),
  Eq (α := R[X]) (C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [C_neg_one, C_one]
  | add_two n ih1 ih2 =>
    have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := C_add_one R n
    have h₂ := C_sub_one R (-n)
    linear_combination (norm := ring_nf) (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]) (C R (↑n.natAbs : ℤ)) (C R n)
have inl : ∀ (h : n = (↑n.natAbs : ℤ)), Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C 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]) (C R (↑n.natAbs : ℤ)) (C R n)
⊢ Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)
have inr : ∀ (h : n = -(↑n.natAbs : ℤ)), Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C 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]) (C R (↑n.natAbs : ℤ)) (C R n)
have inl : Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C 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]) (C R (↑n.natAbs : ℤ)) (C R n)
have inr : Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C 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 :
  comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
ih2 : comp (C R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ))
⊢ comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
have add_two : HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) -
    HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ)) =
  2 * (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ))
Tactic: simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (C R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ)))
ih2 :
  comp (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
⊢ comp (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
have neg_add_one : HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ))) -
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
  2 * (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
Tactic: simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ comp (C R n) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R n)
have zero : comp (C R 0) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 0)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (C R 0) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 0)
⊢ comp (C R n) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R n)
have one : comp (C R 1) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (C R 0) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 0)
one : comp (C R 1) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R 1)
⊢ comp (C R n) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R n)
have add_two : ∀ (n : ℕ)
  (ih1 :
    comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) =
      HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
  (ih2 : comp (C R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = HMul.hMul (α := R[X]) 2 (T R (↑n : ℤ))),
  comp (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
  | neg_add_one n ih1 ih2 =>
    simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
    ring
Cleared hypotheses: n