awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ HMul.hMul (α := R[X]) 2 (T R (n + 2)) = HSub.hSub (α := R[X]) (U R (n + 2)) (U R n)

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)

Premises used: Polynomial.Chebyshev.T_eq_X_mul_U_sub_U, HAdd.hAdd, OfNat.ofNat, Polynomial.Chebyshev.T_eq_U_sub_X_mul_U
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ U R (n + 2) = HMul.hMul (α := R[X]) 2 (T R (n + 2)) + U R n

Tactic:
linear_combination (norm := ring_nf) - (two_mul_T_eq_U_sub_U R n)

Premises used: Polynomial.Chebyshev.two_mul_T_eq_U_sub_U
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 0)) (U R (↑0 : ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ U R (↑1 : ℤ) = HMul.hMul (α := R[X]) 2 (T R 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
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))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 1)) (U R (↑1 : ℤ))

Tactic:
rw [show U R (1 : ℕ) = 2 * T R 1 by simp, ← smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
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))
⊢ 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:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Membership.mem (γ := Set ℕ) (Set.Icc 0 1) 1 ∧ Eq (α := R[X]) ((fun (m : ℕ) ↦ (T R (↑m : ℤ) : R[X])) 1) (T R 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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]) 2 (T R 1))

Tactic:
exact Submodule.smul_of_tower_mem _ 2 (Submodule.mem_span_of_mem ⟨1, by simp⟩)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
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 : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2)))
    (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
rw [U_eq_two_mul_T_add_U, ← smul_eq_mul]

Premises used: Polynomial.Chebyshev.U_eq_two_mul_T_add_U, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
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 : ℤ))
⊢ 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:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
⊢ Subset.{u_1} (α := Set R[X]) ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)
    ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n + 2))

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
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) : ℤ)))
⊢ 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:
refine Submodule.add_mem _ ?_ ((Submodule.span_mono (by grind)) h₀)

Premises used: Submodule.span_mono, Submodule.add_mem
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ))
⊢ n + 2 ∈ Set.Icc 0 (n + 2) ∧ Eq (α := R[X]) ((fun (m : ℕ) ↦ (T R (↑m : ℤ) : R[X])) (n + 2)) (T R (↑(n + 2) : ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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) : ℤ)))

Tactic:
exact Submodule.smul_of_tower_mem _ 2
        (Submodule.mem_span_of_mem ⟨n + 2, by simp⟩)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
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) : ℤ))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 n)) (U R (↑n : ℤ))

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⟩)

Premises used: Polynomial.Chebyshev.U_eq_two_mul_T_add_U, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
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
⊢ 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:
simp [Int.negSucc_eq]

Premises used: Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
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
⊢ C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑(k + 1) : ℤ)) 1)) - C R (-(↑(k + 1) : ℤ))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) C.eq_4 R k

Premises used: Polynomial.Chebyshev.C.eq_4, Int.negSucc_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ C R (n + 1) = HMul.hMul (α := R[X]) X (C R n) - C R (n - 1)

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.C_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ C R (n - 2) = HMul.hMul (α := R[X]) X (C R (n - 1)) - C R n

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.C_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ C R (n - 1) = HMul.hMul (α := R[X]) X (C R n) - C R (n + 1)

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.C_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
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
⊢ C R n = HMul.hMul (α := R[X]) X (C R (n - 1)) - C R (n - 2)

Tactic:
linear_combination (norm := ring_nf) C_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.C_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (C R 0) 2

Tactic:
simp [C]

Premises used: Polynomial.Chebyshev.C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (C R 1) X

Tactic:
simp [C]

Premises used: Polynomial.Chebyshev.C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
rw : HMul.hMul (α := R[X]) X (C R (-(↑0 : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X
⊢ Eq (α := R[X]) (C R (Int.negSucc 0)) X

Tactic:
rw [C]

Premises used: Polynomial.Chebyshev.C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : HMul.hMul (α := R[X]) X 2 - X = X
⊢ HMul.hMul (α := R[X]) X (C R (-(↑0 : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
suffices : HMul.hMul (α := R[X]) X 2 - X = X
⊢ HMul.hMul (α := R[X]) X (C R (-(↑0 : ℤ))) - C R (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1) = X

Tactic:
suffices X * 2 - X = X by simpa
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) X 2 - X = X

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ C R 2 = HPow.hPow (α := R[X]) (β := ℕ) X 2 - 2

Tactic:
simpa [pow_two, mul_assoc] using C_add_two R 0

Premises used: pow_two, mul_assoc, Polynomial.Chebyshev.C_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (C R (-0)) (C R 0)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (C R (-1)) (C R 1)

Tactic:
simp only [C_neg_one, C_one]

Premises used: Polynomial.Chebyshev.C_one, Polynomial.Chebyshev.C_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ)
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
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
⊢ Eq (α := R[X]) (C R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))

Tactic:
linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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
⊢ Eq (α := R[X]) (C R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))

Tactic:
linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ - h₂

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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))
⊢ Eq (α := R[X]) (C R (-n)) (C R n)

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₂

Premises used: Polynomial.Chebyshev.C_one, Polynomial.Chebyshev.C_neg_one, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inl : ∀ (h : n = (↑n.natAbs : ℤ)), Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)
inr : ∀ (h : n = -(↑n.natAbs : ℤ)), Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)
⊢ Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)

Tactic:
obtain h | h := Int.natAbs_eq n

Premises used: Int.natAbs_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = (↑n.natAbs : ℤ)
inl inl₁ : Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R (↑n.natAbs : ℤ))
⊢ Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = -(↑n.natAbs : ℤ)
inr : Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R (-(↑n.natAbs : ℤ)))
⊢ Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R n)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = -(↑n.natAbs : ℤ)
⊢ Eq (α := R[X]) (C R (↑n.natAbs : ℤ)) (C R (-(↑n.natAbs : ℤ)))

Tactic:
simp