awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
⊢ HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))

Tactic:
have h₁ := T_mul_T R ((-m) * n) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
⊢ Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (T R n))
      (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))

Tactic:
have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (T R n))
      (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
⊢ comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
      comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)

Tactic:
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂

Premises used: Polynomial.X_comp, Polynomial.ofNat_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
h₂ :
  comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
      comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)
⊢ T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
        (HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
              (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n)) +
            HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n +
          HMul.hMul (α := R[X]) 2 (T R n) * comp (T R (-(↑m : ℤ))) (T R n)) -
      (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
        (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
              (HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
                comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)) +
            HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n)) +
          HMul.hMul (α := R[X]) 2 (T R n) * T R (-(↑m : ℤ) * n))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
h₂ :
  comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
      comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)
a :
  T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
        (HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
              (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n)) +
            HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n +
          HMul.hMul (α := R[X]) 2 (T R n) * comp (T R (-(↑m : ℤ))) (T R n)) -
      (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
        (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
              (HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
                comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)) +
            HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n)) +
          HMul.hMul (α := R[X]) 2 (T R n) * T R (-(↑m : ℤ) * n))) =
    0
⊢ Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Premises used: Polynomial.Chebyshev.T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m n : ℤ
zero : Eq (α := R[X]) (T R (0 * n)) (comp (T R 0) (T R n))
one : Eq (α := R[X]) (T R (1 * n)) (comp (T R 1) (T R n))
add_two :
  ∀ (m : ℕ)
    (ih1 :
      Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n)))
    (ih2 : Eq (α := R[X]) (T R ((↑m : ℤ) * n)) (comp (T R (↑m : ℤ)) (T R n))),
    Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n))
neg_add_one :
  ∀ (m : ℕ) (ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n)))
    (ih2 :
      Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
        (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))),
    Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
⊢ Eq (α := R[X]) (T R (m * n)) (comp (T R m) (T R n))

Tactic:
induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := T_mul_T R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := T_mul_T R ((-m) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Premises used: Polynomial.Chebyshev.T, Polynomial.X_comp, Polynomial.ofNat_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (C R (0 * n)) (comp (C R 0) (C R n))

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

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
⊢ HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))

Tactic:
have h₁ := C_mul_C R ((m + 1) * n) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
⊢ Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n)) (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) - C R (↑m : ℤ)))

Tactic:
have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n)) (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) - C R (↑m : ℤ)))
⊢ comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) - comp (C R (↑m : ℤ)) (C R n)

Tactic:
simp only [sub_comp, mul_comp, X_comp] at h₂

Premises used: Polynomial.X_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) - comp (C R (↑m : ℤ)) (C R n)
⊢ C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n) +
        (HAdd.hAdd (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n)) +
            HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) +
          HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))) -
      (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) +
        (comp (C R (↑m : ℤ)) (C R n) +
              (HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) -
                comp (C R (↑m : ℤ)) (C R n)) +
            HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n))
              (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n)) +
          HMul.hMul (α := R[X]) (C R n) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) - comp (C R (↑m : ℤ)) (C R n)
a :
  C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n) +
        (HAdd.hAdd (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n)) +
            HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) +
          HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))) -
      (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) +
        (comp (C R (↑m : ℤ)) (C R n) +
              (HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) -
                comp (C R (↑m : ℤ)) (C R n)) +
            HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n))
              (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n)) +
          HMul.hMul (α := R[X]) (C R n) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)))) =
    0
⊢ Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1

Premises used: Polynomial.Chebyshev.C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
⊢ HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))

Tactic:
have h₁ := C_mul_C R ((-m) * n) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
⊢ Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n))
      (HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) - C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))

Tactic:
have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n))
      (HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) - C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
⊢ comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
      comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)

Tactic:
simp only [sub_comp, mul_comp, X_comp] at h₂

Premises used: Polynomial.X_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
h₂ :
  comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
      comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)
⊢ C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
        (HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
              (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n)) +
            HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) +
          HMul.hMul (α := R[X]) (C R n) (comp (C R (-(↑m : ℤ))) (C R n))) -
      (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
        (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
              (HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
                comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)) +
            HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n)) +
          HMul.hMul (α := R[X]) (C R n) (C R (-(↑m : ℤ) * n)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
h₂ :
  comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
      comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)
a :
  C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
        (HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
              (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n)) +
            HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) +
          HMul.hMul (α := R[X]) (C R n) (comp (C R (-(↑m : ℤ))) (C R n))) -
      (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
        (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
              (HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
                comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)) +
            HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n)) +
          HMul.hMul (α := R[X]) (C R n) (C R (-(↑m : ℤ) * n)))) =
    0
⊢ Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1

Premises used: Polynomial.Chebyshev.C
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m n : ℤ
zero : Eq (α := R[X]) (C R (0 * n)) (comp (C R 0) (C R n))
one : Eq (α := R[X]) (C R (1 * n)) (comp (C R 1) (C R n))
add_two :
  ∀ (m : ℕ)
    (ih1 :
      Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)))
    (ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))),
    Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
neg_add_one :
  ∀ (m : ℕ) (ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n)))
    (ih2 :
      Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
        (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))),
    Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
⊢ Eq (α := R[X]) (C R (m * n)) (comp (C R m) (C R n))

Tactic:
induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := C_mul_C R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1

Premises used: Polynomial.X_comp, Polynomial.Chebyshev.C, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
⊢ p.IsPrimitive ↔ ∀ (r : R), (C : (a : R) → R[X]) r ∣ p → IsUnit r

Tactic:
Iff.rfl

Premises used: Iff.rfl, Polynomial.IsPrimitive
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
⊢ IsPrimitive.{u_1} (R := R) 1

Tactic:
fun _ h =>
  isUnit_C.mp (isUnit_of_dvd_one h)

Premises used: Polynomial.IsPrimitive, Polynomial.isUnit_C, isUnit_of_dvd_one, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
rwa : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q).coeff p.natDegree = 1
rwa₁ rwa₂ rwa₃ rwa₄ : p.coeff p.natDegree = 1
⊢ r * q.coeff p.natDegree = 1

Tactic:
rwa [← coeff_C_mul, ← h]

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
⊢ IsUnit r

Tactic:
exact .of_mul_eq_one (q.coeff p.natDegree) (by rwa [← coeff_C_mul, ← h])
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
hp : IsPrimitive.{u_1} (R := R) 0
⊢ False

Tactic:
(hp 0 (dvd_zero (C 0))).ne_zero rfl

Premises used: Polynomial.C, dvd_zero, IsUnit.ne_zero, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
hp : IsPrimitive.{u_1} (R := R) 0
⊢ False

Tactic:
exact (hp 0 (dvd_zero (C 0))).ne_zero rfl

Premises used: Polynomial.C, dvd_zero, IsUnit.ne_zero, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
hp : p.IsPrimitive
hq : q ∣ p
⊢ q.IsPrimitive

Tactic:
fun a ha => isPrimitive_iff_isUnit_of_C_dvd.mp hp a (dvd_trans ha hq)

Premises used: Polynomial.isPrimitive_iff_isUnit_of_C_dvd, Polynomial.IsPrimitive, dvd_trans, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
this : ¬IsUnit q
⊢ IsUnit r

Tactic:
simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff

Premises used: Polynomial.constantCoeff, Irreducible.isUnit_or_isUnit, IsUnit.map, Or.resolve_right
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
suffices : ¬IsUnit q
⊢ IsUnit r

Tactic:
suffices ¬IsUnit q by simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
q : R[X]
H : IsUnit q
hq : p = (C : (a : R) → R[X]) 0 * q
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
H : IsUnit q
⊢ r ≠ 0

Tactic:
have hr : r ≠ 0 := by rintro rfl; simp_all