awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
rw : HPow.hPow (α := R[X]) X n * X * p
| HPow.hPow (α := R[X]) X (n + 1) * p

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X (n + 1) * p = p * HPow.hPow (α := R[X]) X (n + 1)

Tactic:
conv_lhs => rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₂ : HPow.hPow (α := R[X]) X n * p * X = p * HPow.hPow (α := R[X]) X (n + 1)
succ₃ : p * HPow.hPow (α := R[X]) X n * X = p * HPow.hPow (α := R[X]) X (n + 1)
succ₄ : p * (HPow.hPow (α := R[X]) X n * X) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₅ succ₆ : p * HPow.hPow (α := R[X]) X (n + 1) = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)

Tactic:
rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

Premises used: pow_succ, mul_assoc, Polynomial.X_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : HPow.hPow (α := R[X]) (β := ℕ) X 0 * p = p * HPow.hPow (α := R[X]) (β := ℕ) X 0
succ :
  ∀ (n : ℕ) (ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n),
    HPow.hPow (α := R[X]) X (n + 1) * p = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs => rw [pow_succ]
    rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

Premises used: pow_succ, mul_assoc, Polynomial.X_mul, AddMonoidAlgebra.zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
r : R
⊢ HMul.hMul (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X

Tactic:
X_mul

Premises used: Polynomial.X_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
r : R
n : ℕ
⊢ HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)

Tactic:
X_pow_mul

Premises used: Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : p * (HPow.hPow (α := R[X]) X n * q) = p * q * HPow.hPow (α := R[X]) X n
rw₁ : p * (q * HPow.hPow (α := R[X]) X n) = p * q * HPow.hPow (α := R[X]) X n
rw₂ rw₃ : p * q * HPow.hPow (α := R[X]) X n = p * q * HPow.hPow (α := R[X]) X n
⊢ p * HPow.hPow (α := R[X]) X n * q = p * q * HPow.hPow (α := R[X]) X n

Tactic:
rw [mul_assoc, X_pow_mul, ← mul_assoc]

Premises used: mul_assoc, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
r : R
⊢ HMul.hMul (β := R[X]) (p * HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X]) =
    HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) * HPow.hPow (α := R[X]) X n

Tactic:
X_pow_mul_assoc

Premises used: Polynomial.X_pow_mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ Commute X p

Tactic:
X_mul

Premises used: SemiconjBy, Commute, Polynomial.X_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ Commute (HPow.hPow (α := R[X]) X n) p

Tactic:
X_pow_mul

Premises used: SemiconjBy, Commute, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) r
rw₁ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (r * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
rw₂ rw₃ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r

Tactic:
rw [X, monomial_mul_monomial, mul_one]

Premises used: mul_one, Polynomial.X, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) =
    (monomial (n + 0) : (a : R) → R[X]) r

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
ih :
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (k + 1)) =
    (monomial (n + (k + 1)) : (a : R) → R[X]) r

Tactic:
simp [ih, pow_succ, ← mul_assoc, add_assoc]

Premises used: pow_succ, add_assoc, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
zero :
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) =
    (monomial (n + 0) : (a : R) → R[X]) r
succ :
  ∀ (k : ℕ)
    (ih :
      HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
        (monomial (n + k) : (a : R) → R[X]) r),
    HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (k + 1)) =
      (monomial (n + (k + 1)) : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

Premises used: pow_succ, add_assoc, mul_assoc, AddMonoidAlgebra.zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
rw₁ rw₂ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
⊢ HMul.hMul (α := R[X]) (β := R[X]) X ((monomial n : (a : R) → R[X]) r : R[X]) = (monomial (n + 1) : (a : R) → R[X]) r

Tactic:
rw [X_mul, monomial_mul_X]

Premises used: Polynomial.monomial_mul_X, Polynomial.X_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r
rw₁ rw₂ : Eq (α := R[X]) ((monomial (n + k) : (a : R) → R[X]) r : R[X]) ((monomial (n + k) : (a : R) → R[X]) r : R[X])
⊢ HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X k) ((monomial n : (a : R) → R[X]) r : R[X]) =
    (monomial (n + k) : (a : R) → R[X]) r

Tactic:
rw [X_pow_mul, monomial_mul_X_pow]

Premises used: Polynomial.monomial_mul_X_pow, Polynomial.X_pow_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[ℕ]
rw rw₁ : Eq (α := ℕ → R) (⇑p : (a : ℕ) → R) (⇑p : (a : ℕ) → R)
⊢ { toFinsupp := p : R[X] }.coeff = (⇑p : (a : ℕ) → R)

Tactic:
rw [coeff]

Premises used: Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[ℕ]
⊢ { toFinsupp := p : R[X] }.coeff = { toFinsupp := q : R[X] }.coeff → { toFinsupp := p : R[X] } = { toFinsupp := q }

Tactic:
simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

Premises used: Polynomial.coeff, DFunLike.coe_fn_eq, imp_self, Polynomial.ofFinsupp.injEq
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.coeff = q.coeff ↔ p = q

Tactic:
coeff_injective.eq_iff

Premises used: Function.Injective.eq_iff, Polynomial.coeff_injective
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
f : R[X]
i : ℕ
ofFinsupp :
  ∀ (toFinsupp : R[ℕ]),
    ({ toFinsupp := toFinsupp : R[X] }.toFinsupp : (a : ℕ) → R) i = { toFinsupp := toFinsupp : R[X] }.coeff i
⊢ (f.toFinsupp : (a : ℕ) → R) i = f.coeff i

Tactic:
cases f
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
i : ℕ
toFinsupp : R[ℕ]
⊢ ({ toFinsupp := toFinsupp : R[X] }.toFinsupp : (a : ℕ) → R) i = { toFinsupp := toFinsupp : R[X] }.coeff i

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
f : R[X]
⊢ (Set.range f.coeff).Finite

Tactic:
Finsupp.finite_range _

Premises used: Finsupp.finite_range, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
m n : ℕ
inst : Semiring R
⊢ coeff ((monomial n : (a : R) → R[X]) a) m = if n = m then a else 0

Tactic:
simp [coeff, Finsupp.single_apply]

Premises used: Polynomial.coeff, Finsupp.single_apply
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
⊢ coeff ((monomial n : (a : R) → R[X]) c) n = c

Tactic:
Finsupp.single_eq_same

Premises used: Finsupp.single_eq_same, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
m n : ℕ
c : R
h : m ≠ n
⊢ Eq.{u + 1} (α := R) (coeff ((monomial n : (a : R) → R[X]) c) m) 0

Tactic:
Finsupp.single_eq_of_ne h

Premises used: Finsupp.single_eq_of_ne, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff 0 n) 0

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
simp_rw : Eq.{u + 1} (α := R) (coeff 1 n) (if 0 = n then 1 else 0)
⊢ Eq.{u + 1} (α := R) (coeff 1 n) (if n = 0 then 1 else 0)

Tactic:
simp_rw [eq_comm (a := n) (b := 0)]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff 1 n) (if 0 = n then 1 else 0)

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff 1 n) (if 0 = n then 1 else 0)

Tactic:
exact coeff_monomial

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff 1 0) 1

Tactic:
simp [coeff_one]

Premises used: Polynomial.coeff_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff X 1) 1

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial, Polynomial.X, ite
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff X 0) 0

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial, Polynomial.X, ite
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff ((monomial (n + 1) : (a : R) → R[X]) a) 0) 0

Tactic:
simp [coeff_monomial]

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
n : ℕ
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff X n) (if 1 = n then 1 else 0)

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 1
rw : Eq.{u + 1} (α := R) (if 1 = n then 1 else 0) 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (coeff X n) 0

Tactic:
rw [coeff_X, if_neg hn.symm]

Premises used: Ne.symm, Polynomial.coeff_X, if_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
rcases :
  ∀ (toFinsupp : R[ℕ]), n ∈ { toFinsupp := toFinsupp : R[X] }.support ↔ { toFinsupp := toFinsupp : R[X] }.coeff n ≠ 0
⊢ n ∈ p.support ↔ p.coeff n ≠ 0

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
n : ℕ
inst : Semiring R
toFinsupp : R[ℕ]
⊢ n ∈ { toFinsupp := toFinsupp : R[X] }.support ↔ { toFinsupp := toFinsupp : R[X] }.coeff n ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ coeff ((monomial 0 : (a : R) → R[X]) a) n = if 0 = n then a else 0

Tactic:
coeff_monomial (a := a) (m := n) (n := 0)

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
h : n = 0 ↔ 0 = n
⊢ coeff ((C : (a : R) → R[X]) a) n = if n = 0 then a else 0

Tactic:
convert! coeff_monomial (a := a) (m := n) (n := 0) using 2

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ n = 0 ↔ 0 = n

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Semiring R
⊢ coeff ((C : (a : R) → R[X]) a) 0 = a

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial, ite
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
h : n ≠ 0
rw : (if n = 0 then a else 0) = 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (coeff ((C : (a : R) → R[X]) a) n) 0

Tactic:
rw [coeff_C, if_neg h]

Premises used: Polynomial.coeff_C, if_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
r : R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff ((C : (a : R) → R[X]) r) (n + 1)) 0

Tactic:
simp [coeff_C]

Premises used: Polynomial.coeff_C
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
m n : ℕ
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff (↑m : R[X]) n) (↑(if n = 0 then m else 0) : R)

Tactic:
simp only [← C_eq_natCast, coeff_C, Nat.cast_ite, Nat.cast_zero]

Premises used: Polynomial.C_eq_natCast, Polynomial.coeff_C, Nat.cast_ite, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : ℕ
inst_1 : a.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (coeff (OfNat.ofNat a) 0) (OfNat.ofNat a)

Tactic:
coeff_monomial

Premises used: Polynomial.coeff_monomial, Finsupp.single, ite
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a n : ℕ
h : a.AtLeastTwo
rw : Eq.{u + 1} (α := R) (coeff (↑(OfNat.ofNat a) : R[X]) (n + 1)) 0
⊢ Eq.{u + 1} (α := R) (coeff (OfNat.ofNat a) (n + 1)) 0

Tactic:
rw [← Nat.cast_ofNat]

Premises used: Nat.cast_ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (coeff (↑(OfNat.ofNat a) : R[X]) (n + 1)) 0

Tactic:
simp [-Nat.cast_ofNat]

Premises used: Nat.cast_ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) a
rw₃ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₄ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (a * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X])
rw₅ rw₆ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a

Tactic:
rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

Premises used: pow_succ, mul_assoc, mul_one, Polynomial.X, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw : Eq (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) a)) (single n a)
rw₁ rw₂ : Eq (α := R[ℕ]) (single n a) (single n a)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).toFinsupp = single n a

Tactic:
rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Semiring R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)
rw₁ rw₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X = (monomial 1 : (a : R) → R[X]) a

Tactic:
rw [← C_mul_X_pow_eq_monomial, pow_one]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, pow_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
rw : Eq (α := R[ℕ]) (toFinsupp ((monomial 1 : (a : R) → R[X]) a)) (single 1 a)
rw₁ rw₂ : Eq (α := R[ℕ]) (single 1 a) (single 1 a)
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).toFinsupp = single 1 a

Tactic:
rw [C_mul_X_eq_monomial, toFinsupp_monomial]

Premises used: Polynomial.C_mul_X_eq_monomial, Polynomial.toFinsupp_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Injective.{u + 1, u + 1} (α := R) (β := R[X]) (⇑C : (a : R) → R[X])

Tactic:
monomial_injective 0

Premises used: Polynomial.monomial_injective, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X]) ↔ a = b

Tactic:
C_injective.eq_iff

Premises used: Function.Injective.eq_iff, Polynomial.C_injective
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Semiring R
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X]) ↔ a = 0

Tactic:
C_injective.eq_iff' (map_zero C)

Premises used: Polynomial.C, map_zero, Function.Injective.eq_iff', Polynomial.C_injective
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
inst : Semiring R
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X]) ↔ a ≠ 0

Tactic:
C_eq_zero.not

Premises used: Polynomial.C_eq_zero, Iff.not
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
h : Subsingleton R
⊢ Subsingleton.{u + 1} R[X]

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p ≠ q
⊢ Nontrivial R

Tactic:
(subsingleton_or_nontrivial R).resolve_left fun _hI => h <| Subsingleton.elim _ _

Premises used: subsingleton_or_nontrivial, Or.resolve_left, Subsingleton.elim
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

Premises used: subsingleton_iff, Polynomial.subsingleton_iff_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rcases : ∀ (f : ℕ →₀ R), { toFinsupp := f : R[X] } = q ↔ ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = q.coeff n
⊢ p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : ℕ →₀ R⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
q : R[X]
f : ℕ →₀ R
rcases :
  ∀ (g : ℕ →₀ R),
    { toFinsupp := f : R[X] } = { toFinsupp := g } ↔
      ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = { toFinsupp := g : R[X] }.coeff n
⊢ { toFinsupp := f : R[X] } = q ↔ ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = q.coeff n

Tactic:
rcases q with ⟨g : ℕ →₀ R⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
f g : ℕ →₀ R
⊢ { toFinsupp := f : R[X] } = { toFinsupp := g } ↔
    ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = { toFinsupp := g : R[X] }.coeff n

Tactic:
simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

Premises used: DFunLike.ext_iff, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q

Tactic:
ext_iff.2

Premises used: Iff.mpr, Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
h :
  LE.le.{u} (α := AddSubmonoid R[X]) ⊤
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
⊢ Eq.{u + 1} (α := AddSubmonoid R[X])
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a}) ⊤

Tactic:
apply top_unique

Premises used: top_unique
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
h :
  LE.le (α := AddSubmonoid R[X])
    (AddSubmonoid.closure
      (Set.image (α := R[ℕ]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
        {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}))
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
⊢ LE.le.{u} (α := AddSubmonoid R[X]) ⊤
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})

Tactic:
rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ←
    Finsupp.add_closure_setOf_eq_single, AddMonoidHom.map_mclosure]

Premises used: RingEquiv.toAddEquiv, AddSubmonoid.map_equiv_top, AddMonoidHom.map_mclosure, Polynomial.toFinsuppIso, Finsupp.add_closure_setOf_eq_single, RingEquiv.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ LE.le (α := AddSubmonoid R[X])
    (AddSubmonoid.closure
      (Set.image (α := R[ℕ]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
        {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}))
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})

Tactic:
AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)

Premises used: Iff.mpr, Set.image_subset_iff, AddSubmonoid.closure_mono
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
h :
  Subset (α := Set R[ℕ]) {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}
    (Set.preimage (β := R[X]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
      {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
⊢ LE.le (α := AddSubmonoid R[X])
    (AddSubmonoid.closure
      (Set.image (α := R[ℕ]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
        {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}))
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})

Tactic:
refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)

Premises used: Iff.mpr, Set.image_subset_iff, AddSubmonoid.closure_mono
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ Membership.mem (γ := Set R[ℕ])
    (Set.preimage (β := R[X]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
      {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
    (Finsupp.single n a)

Tactic:
⟨n, a, Polynomial.ofFinsupp_single _ _⟩

Premises used: Set.Mem, Polynomial.ofFinsupp_single, setOf, Set.preimage, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ Membership.mem (γ := Set R[ℕ])
    (Set.preimage (β := R[X]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
      {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
    (Finsupp.single n a)

Tactic:
exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩