awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
rw :
  ∑ x ∈ range (n + 1),
      (lcoeff R k : (a : R[X]) → R)
        (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (n - x) *
          (↑(n.choose x) : R[X])) =
    r ^ (n - k) * (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n).coeff k = r ^ (n - k) * (↑(n.choose k) : R)

Tactic:
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]

Premises used: Polynomial.C, Commute.add_pow, Polynomial.lcoeff_apply, map_sum, Polynomial.commute_X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
simp :
  ∑ x ∈ range (n + 1), (HPow.hPow (α := R[X]) X x).coeff k * r ^ (n - x) * (↑(n.choose x) : R) =
    r ^ (n - k) * (↑(n.choose k) : R)
⊢ ∑ x ∈ range (n + 1),
      (lcoeff R k : (a : R[X]) → R)
        (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (n - x) *
          (↑(n.choose x) : R[X])) =
    r ^ (n - k) * (↑(n.choose k) : R)

Tactic:
simp only [lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C]

Premises used: Polynomial.C_eq_natCast, Polynomial.lcoeff_apply, Polynomial.coeff_mul_C, Polynomial.C_pow
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h₀ : ∀ b ∈ range (n + 1), b ≠ k → (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0
h₁ : k ∉ range (n + 1) → (HPow.hPow (α := R[X]) X k).coeff k * r ^ (n - k) * (↑(n.choose k) : R) = 0
⊢ ∑ x ∈ range (n + 1), (HPow.hPow (α := R[X]) X x).coeff k * r ^ (n - x) * (↑(n.choose x) : R) =
    r ^ (n - k) * (↑(n.choose k) : R)

Tactic:
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]

Premises used: Finset.sum_eq_single, Polynomial.coeff_X_pow_self, one_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k b : ℕ
h₀ : b ∈ range (n + 1) → b ≠ k → (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0
⊢ b ∈ range (n + 1) → b ≠ k → (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k b : ℕ
h_1 : b ∈ range (n + 1)
h : b ≠ k
⊢ (HPow.hPow (α := R[X]) X b).coeff k * r ^ (n - b) * (↑(n.choose b) : R) = 0

Tactic:
simp [coeff_X_pow, h.symm]

Premises used: Polynomial.coeff_X_pow, Ne.symm
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h₁ : n + 1 ≤ k → r ^ (n - k) * (↑(n.choose k) : R) = 0
⊢ k ∉ range (n + 1) → (HPow.hPow (α := R[X]) X k).coeff k * r ^ (n - k) * (↑(n.choose k) : R) = 0

Tactic:
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]

Premises used: Finset.mem_range, Polynomial.coeff_X_pow_self, not_lt, one_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
h₁ : r ^ (n - k) * (↑0 : R) = 0
h₂ : r ^ (n - k) * 0 = 0
h₃ h₄ : Eq.{u + 1} (α := R) 0 0
⊢ r ^ (n - k) * (↑(n.choose k) : R) = 0

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) ^ n).coeff k = (↑(n.choose k) : R)
rw₁ : HPow.hPow (α := R) 1 (n - k) * (↑(n.choose k) : R) = (↑(n.choose k) : R)
rw₂ : HMul.hMul (α := R) 1 (↑(n.choose k) : R) = (↑(n.choose k) : R)
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) (↑(n.choose k) : R) (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)

Tactic:
rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]

Premises used: one_pow, Polynomial.C_1, one_mul, Polynomial.coeff_X_add_C_pow
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Semiring R
n k : ℕ
rw : (HAdd.hAdd (α := R[X]) X 1 ^ n).coeff k = (↑(n.choose k) : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (↑(n.choose k) : R) (↑(n.choose k) : R)
⊢ (HAdd.hAdd (α := R[X]) 1 X ^ n).coeff k = (↑(n.choose k) : R)

Tactic:
rw [add_comm _ X, coeff_X_add_one_pow]

Premises used: add_comm, Polynomial.coeff_X_add_one_pow, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
a :
  ∀ (i : ℕ),
    (HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d).coeff i =
      coeff (∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i) i
⊢ HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d = ∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
a : HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0
⊢ (HAdd.hAdd (α := S[X]) 1 X ^ d - HPow.hPow (α := S[X]) X d).coeff i =
    coeff (∑ i ∈ range d, d.choose i • HPow.hPow (α := S[X]) X i) i

Tactic:
simp [Polynomial.coeff_one_add_X_pow]

Premises used: Polynomial.coeff_one_add_X_pow
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
pos : i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)
neg : i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 1 = 0
pos₁ : ¬i = d → i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 0 = (↑(d.choose i) : S)
neg₁ : ¬i = d → ¬i < d → HSub.hSub (α := S) (↑(d.choose i) : S) 0 = 0
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) (if i = d then 1 else 0) = if i < d then (↑(d.choose i) : S) else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
h : i = d
h_1 : i < d
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) 1 = (↑(d.choose i) : S)

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
h : i = d
h_1 : ¬i < d
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) 1 = 0

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
h : ¬i = d
h_1 : i < d
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) 0 = (↑(d.choose i) : S)

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
S : Type u_1
inst : CommRing S
d i : ℕ
h : ¬i = d
h_1 : ¬i < d
⊢ HSub.hSub (α := S) (↑(d.choose i) : S) 0 = 0

Tactic:
simp_all [Nat.choose_eq_zero_of_lt, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
mp : (C : (a : R) → R[X]) r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i
mpr : (∀ (i : ℕ), r ∣ φ.coeff i) → (C : (a : R) → R[X]) r ∣ φ
⊢ (C : (a : R) → R[X]) r ∣ φ ↔ ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : ℕ
mp : r ∣ r * φ.coeff c
⊢ r ∣ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) φ).coeff c

Tactic:
rw [coeff_C_mul]

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * φ.coeff c

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ φ.coeff i
mpr : ∀ (c : (i : ℕ) → R) (hc : ∀ (i : ℕ), φ.coeff i = r * c i), (C : (a : R) → R[X]) r ∣ φ
⊢ (C : (a : R) → R[X]) r ∣ φ

Tactic:
choose c hc using h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
h : φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
⊢ (C : (a : R) → R[X]) r ∣ φ

Tactic:
use ψ
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
h : ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
⊢ φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
h : φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
⊢ φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i

Tactic:
simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']

Premises used: Finset.sum_ite_eq', Polynomial.coeff_C_mul, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
pos : ∀ (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
neg : ∀ (hi : ¬φ.coeff i ≠ 0), φ.coeff i = r * 0
⊢ φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0

Tactic:
split_ifs with hi
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
pos pos₁ : r * c i = r * c i
⊢ φ.coeff i = r * c i

Tactic:
rw [hc]
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = 0

Tactic:
rw [Classical.not_not] at hi

Premises used: Classical.not_not
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i)
i : ℕ
hi neg neg₁ neg₂ neg₃ : φ.coeff i = 0
⊢ φ.coeff i = r * 0

Tactic:
rwa [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
r : R
φ : R[X]
c : (i : ℕ) → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
mpr mpr₁ mpr₂ mpr₃ : (C : (a : R) → R[X]) r ∣ φ
h :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  φ = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ
h₁ :
  let c' : ℕ → R := fun (i : ℕ) ↦ if i ∈ φ.support then c i else 0;
  let ψ : R[X] := ∑ i ∈ φ.support, (monomial i : (a : R) → R[X]) (c' i);
  ∀ (i : ℕ), φ.coeff i = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ψ).coeff i
h₂ : ∀ (i : ℕ), φ.coeff i = r * if φ.coeff i ≠ 0 then if φ.coeff i ≠ 0 then c i else 0 else 0
pos : ∀ (i : ℕ) (hi : φ.coeff i ≠ 0), φ.coeff i = r * c i
neg neg₁ : ∀ (i : ℕ) (hi : ¬φ.coeff i ≠ 0), φ.coeff i = r * 0
⊢ (C : (a : R) → R[X]) r ∣ φ

Tactic:
classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finsetSum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]

Premises used: Finset.sum_ite_eq', Classical.not_not, Polynomial.coeff_C_mul, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Polynomial.coeff_monomial, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
⊢ a • p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p

Tactic:
simp [ext_iff]

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
a₁ :
  ∀ (n_1 : ℕ),
    (p.update n a).coeff n_1 =
      (p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n_1
⊢ p.update n a = p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
a₁ : (if n_1 = n then a else p.coeff n_1) = p.coeff n_1 + if n_1 = n then a - p.coeff n else 0
⊢ (p.update n a).coeff n_1 =
    (p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n_1

Tactic:
rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]

Premises used: Polynomial.coeff_update_apply, Polynomial.coeff_add, Polynomial.coeff_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
pos : ∀ (h : n_1 = n), a = p.coeff n_1 + (a - p.coeff n)
neg : ∀ (h : ¬n_1 = n), p.coeff n_1 = p.coeff n_1 + 0
⊢ (if n_1 = n then a else p.coeff n_1) = p.coeff n_1 + if n_1 = n then a - p.coeff n else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
h : n_1 = n
⊢ a = p.coeff n_1 + (a - p.coeff n)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
h : ¬n_1 = n
⊢ p.coeff n_1 = p.coeff n_1 + 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
n : ℕ
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑n : R[X]) 0) (↑n : R)

Tactic:
simp only [coeff_natCast_ite, ite_true]

Premises used: Polynomial.coeff_natCast_ite, ite_true
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
mpr : m = n → Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)

Tactic:
apply_fun fun p => p.coeff 0 at h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)
⊢ m = n

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑m : R[X])

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
i : ℤ
R : Type u_1
inst : Ring R
ofNat : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (coeff (↑(Int.ofNat a) : R[X]) 0) (↑(Int.ofNat a) : R)
negSucc : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (coeff (↑(Int.negSucc a) : R[X]) 0) (↑(Int.negSucc a) : R)
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑i : R[X]) 0) (↑i : R)

Tactic:
cases i
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
a : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑(Int.ofNat a) : R[X]) 0) (↑(Int.ofNat a) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u_1
inst : Ring R
a : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑(Int.negSucc a) : R[X]) 0) (↑(Int.negSucc a) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
mpr : m = n → Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)

Tactic:
apply_fun fun p => p.coeff 0 at h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)
⊢ m = n

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
m : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑m : R[X])

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Coeff
Goal:
R : Type u
S : Type v
a b : R
n_1 m : ℕ
inst : Semiring R
p_1 q r : R[X]
p : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R) (↑n : R) 0
rw₁ :
  Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0)
rw₂ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) (↑n : R[X]) ((C : (a : R) → R[X]) 0)
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n

Tactic:
rw [← CharP.cast_eq_zero_iff R, ← C_inj (R := R), map_natCast, C_0]

Premises used: Polynomial.C_inj, Polynomial.C_0, map_natCast, CharP.cast_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := List R) (coeffList 0) []

Tactic:
simp [coeffList]

Premises used: Polynomial.coeffList
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ P.coeffList = [] ↔ P = 0

Tactic:
simp [coeffList]

Premises used: Polynomial.coeffList
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
h : x ≠ 0
⊢ coeffList ((C : (a : R) → R[X]) x) = [x]

Tactic:
simp [coeffList, List.range_succ, degree_eq_natDegree (C_ne_zero.mpr h)]

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Polynomial.coeffList, Polynomial.C_ne_zero, List.range_succ
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
⊢ ∃ (ls : List R), P.coeffList = P.leadingCoeff :: ls

Tactic:
simp [coeffList, List.range_succ, withBotSucc_degree_eq_natDegree_add_one h]

Premises used: Polynomial.coeffList, Polynomial.withBotSucc_degree_eq_natDegree_add_one, List.range_succ
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList.head? = some P.leadingCoeff

Tactic:
(coeffList_eq_cons_leadingCoeff h).casesOn fun _ ↦ (Eq.symm · ▸ rfl)

Premises used: Polynomial.coeffList_eq_cons_leadingCoeff, Exists.casesOn
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
hP : P.coeffList ≠ []
⊢ P.coeffList.head hP = P.leadingCoeff

Tactic:
let h := coeffList_eq_nil.not.mp hP
  (coeffList_eq_cons_leadingCoeff h).casesOn fun _ _ ↦
    Option.some.injEq _ _ ▸ List.head?_eq_some_head _ ▸ head?_coeffList h

Premises used: Polynomial.coeffList_eq_cons_leadingCoeff, Iff.not, Exists.casesOn, Polynomial.coeffList_eq_nil, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ P.coeffList.length = P.degree.succ

Tactic:
simp [coeffList]

Premises used: Polynomial.coeffList
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
P : R[X]
pos : ∀ (h : P = 0), P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
neg : ∀ (h : ¬P = 0), P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
by_cases h : P = 0
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
P : R[X]
h : P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
simp [h, coeffList, withBotSucc_degree_eq_natDegree_add_one]

Premises used: Polynomial.coeffList, Polynomial.withBotSucc_degree_eq_natDegree_add_one
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
P : R[X]
h : ¬P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
simp [h, coeffList, withBotSucc_degree_eq_natDegree_add_one]

Premises used: Polynomial.coeffList, Polynomial.withBotSucc_degree_eq_natDegree_add_one
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
⊢ P ≠ 0

Tactic:
have h₂ := ne_zero_of_natDegree_gt (natDegree_pos_of_nextCoeff_ne_zero h)
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
⊢ ¬P.eraseLead = 0

Tactic:
have h₃ := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
h₃ : ¬P.eraseLead = 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

Tactic:
simpa [natDegree_eraseLead_add_one h, coeffList, withBotSucc_degree_eq_natDegree_add_one h₂,
    withBotSucc_degree_eq_natDegree_add_one h₃, List.range_succ] using
    (Polynomial.eraseLead_coeff_of_ne · ·.ne)

Premises used: Polynomial.natDegree_eraseLead_add_one, Polynomial.coeffList, Polynomial.withBotSucc_degree_eq_natDegree_add_one, Polynomial.eraseLead_coeff_of_ne, List.range_succ
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
⊢ ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])

Tactic:
have h := mt (Polynomial.monomial_eq_zero_iff x n).mp hx
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
⊢ List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)) = (x :: List.replicate n 0).length

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
⊢ List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)) = (x :: List.replicate n 0).length

Tactic:
classical simp [hx]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
apply :
  ∀ (n_1 : ℕ) (h₁ : n_1 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))
    (h₂ : n_1 < (x :: List.replicate n 0).length),
    List.get (coeffList ((monomial n : (a : R) → R[X]) x))
        (⟨n_1, h₁⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
      (x :: List.replicate n 0).get (⟨n_1, h₂⟩ : Fin (x :: List.replicate n 0).length)
⊢ coeffList ((monomial n : (a : R) → R[X]) x) = x :: List.replicate n 0

Tactic:
apply List.ext_get (by classical simp [hx])

Premises used: List.ext_get
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
h₁_1 : 0 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x))
h₁ : 0 < (x :: List.replicate n 0).length
⊢ ∀ (w : List R)
    (h : coeffList ((monomial n : (a : R) → R[X]) x) = leadingCoeff ((monomial n : (a : R) → R[X]) x) :: w),
    List.get (coeffList ((monomial n : (a : R) → R[X]) x))
        (⟨0, h₁_1⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
      (x :: List.replicate n 0).get (⟨0, h₁⟩ : Fin (x :: List.replicate n 0).length)

Tactic:
simp_all