awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
n : ℕ
a : R
zero : motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0))
succ :
  ∀ (n : ℕ)
    (ih : motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih

Premises used: pow_zero, AddMonoidAlgebra.zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
have :
  ∀
    (A :
      ∀ {n : ℕ} {a : R},
        motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))),
    motive p
⊢ motive p

Tactic:
have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) := by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
empty :
  motive
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
insert :
  ∀ (a : ℕ) (s : Finset ℕ),
    a ∉ s →
      motive
          (∑ n ∈ s,
            HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)) →
        motive
          (∑ n ∈ Insert.insert a s,
            HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
apply Finset.induction
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive ((Polynomial.C : (a : R) → R[X]) 0)

Tactic:
C 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
h :
  Eq.{u + 1} (α := R[X])
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
    ((Polynomial.C : (a : R) → R[X]) 0)
⊢ motive
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
convert! C 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq.{u + 1} (α := R[X])
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
    ((Polynomial.C : (a : R) → R[X]) 0)

Tactic:
C_0.symm

Premises used: Multiset.sum, Multiset.foldr, Polynomial.C_0, Eq.symm, List.foldr, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq.{u + 1} (α := R[X])
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
    ((Polynomial.C : (a : R) → R[X]) 0)

Tactic:
exact C_0.symm

Premises used: Polynomial.C_0, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih :
  motive
    (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
insert :
  motive
    (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) +
      ∑ x ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
⊢ motive
    (∑ n ∈ Insert.insert n s,
      HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
rw [sum_insert ns]

Premises used: Finset.sum_insert
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih :
  motive
    (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) +
      ∑ x ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))

Tactic:
add _ _ A ih
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih :
  motive
    (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) +
      ∑ x ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))

Tactic:
exact add _ _ A ih
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ => Polynomial.C (p.coeff n) * X ^ n) := by
    apply Finset.induction
    · convert! C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
B :
  ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
rw :
  motive
    (∑ n ∈ p.support,
      HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive p

Tactic:
rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]

Premises used: Polynomial.sum, Polynomial.sum_C_mul_X_pow_eq
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
B :
  ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (∑ n ∈ p.support,
      HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
B (support p)

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
B :
  ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (∑ n ∈ p.support,
      HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
exact B (support p)

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
_h : motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
rw : motive ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a)
⊢ motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
rw [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
_h : motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a)

Tactic:
monomial _ _
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
_h : motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a)

Tactic:
exact monomial _ _
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = AddMonoidAlgebra.erase n p.toFinsupp

Tactic:
simp only [erase_def]

Premises used: Polynomial.erase_def
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[ℕ]
n : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.erase n p : R[X] } = erase n { toFinsupp := p }

Tactic:
simp only [erase_def]

Premises used: Polynomial.erase_def
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support = p.support.erase n

Tactic:
simp only [support, erase_def, Finsupp.support_erase, AddMonoidAlgebra.erase, ofCoeff,
    AddMonoidAlgebra.coeff]

Premises used: AddMonoidAlgebra.coeff, Finsupp.support_erase, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.erase, Polynomial.support, Polynomial.erase_def
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw :
  HAdd.hAdd (α := R[ℕ]) (single n ((p.toFinsupp : (a : ℕ) → R) n) : R[ℕ]) (AddMonoidAlgebra.erase n p.toFinsupp) =
    p.toFinsupp
⊢ (HAdd.hAdd (α := R[X]) ((monomial n : (a : R) → R[X]) (p.coeff n) : R[X]) (erase n p)).toFinsupp = p.toFinsupp

Tactic:
rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.coeff, Polynomial.toFinsupp_add, Polynomial.toFinsupp_erase
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ HAdd.hAdd (α := R[ℕ]) (single n ((p.toFinsupp : (a : ℕ) → R) n) : R[ℕ]) (AddMonoidAlgebra.erase n p.toFinsupp) =
    p.toFinsupp

Tactic:
Finsupp.single_add_erase _ _

Premises used: Finsupp.erase, Finsupp.single_add_erase, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra, AddMonoidAlgebra.erase
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ HAdd.hAdd (α := R[ℕ]) (single n ((p.toFinsupp : (a : ℕ) → R) n) : R[ℕ]) (AddMonoidAlgebra.erase n p.toFinsupp) =
    p.toFinsupp

Tactic:
exact Finsupp.single_add_erase _ _

Premises used: Finsupp.single_add_erase
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n i : ℕ
rcases :
  ∀ (toFinsupp : R[ℕ]),
    (erase n { toFinsupp := toFinsupp : R[X] }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp : R[X] }.coeff i
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
toFinsupp : R[ℕ]
simp :
  Eq (α := R) ((AddMonoidAlgebra.erase n toFinsupp : (a : ℕ) → R) i : R)
    (if i = n then 0 else (toFinsupp : (a : ℕ) → R) i : R)
⊢ (erase n { toFinsupp := toFinsupp : R[X] }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp : R[X] }.coeff i

Tactic:
simp only [erase_def, coeff]

Premises used: Polynomial.coeff, Polynomial.erase_def
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
toFinsupp : R[ℕ]
⊢ Eq (α := R) ((AddMonoidAlgebra.erase n toFinsupp : (a : ℕ) → R) i : R)
    (if i = n then 0 else (toFinsupp : (a : ℕ) → R) i : R)

Tactic:
ite_congr rfl (fun _ => rfl) (fun _ => rfl)

Premises used: ite_congr, rfl, ite
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
toFinsupp : R[ℕ]
⊢ Eq (α := R) ((AddMonoidAlgebra.erase n toFinsupp : (a : ℕ) → R) i : R)
    (if i = n then 0 else (toFinsupp : (a : ℕ) → R) i : R)

Tactic:
exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)

Premises used: ite_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (erase n 0)) (toFinsupp 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (erase n ((monomial n : (a : R) → R[X]) a))) (toFinsupp 0)

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

Tactic:
simp [coeff_erase]

Premises used: Polynomial.coeff_erase
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n i : ℕ
h : i ≠ n
⊢ (erase n p).coeff i = p.coeff i

Tactic:
simp [coeff_erase, h]

Premises used: Polynomial.coeff_erase
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : ∀ (x : ℕ), (p.update n a).coeff x = Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a x
⊢ (p.update n a).coeff = Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
x : ℕ
⊢ (p.update n a).coeff x = Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a x

Tactic:
simp only [coeff, update, Function.update_apply, coe_update, AddMonoidAlgebra.update, ofCoeff,
    AddMonoidAlgebra.coeff]

Premises used: Polynomial.update, AddMonoidAlgebra.coeff, Function.update_apply, Finsupp.coe_update, Polynomial.coeff, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.update
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
rw : Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a i = if i = n then a else p.coeff i
rw₁ rw₂ : (if i = n then a else p.coeff i) = if i = n then a else p.coeff i
⊢ (p.update n a).coeff i = if i = n then a else p.coeff i

Tactic:
rw [coeff_update, Function.update_apply]

Premises used: Function.update_apply, Polynomial.coeff_update
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (if n = n then a else p.coeff n) = a
rw₁ rw₂ : a = a
⊢ (p.update n a).coeff n = a

Tactic:
rw [p.coeff_update_apply, if_pos rfl]

Premises used: Polynomial.coeff_update_apply, if_pos, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
rw : (if i = n then a else p.coeff i) = p.coeff i
rw₁ rw₂ : p.coeff i = p.coeff i
⊢ (p.update n a).coeff i = p.coeff i

Tactic:
rw [p.coeff_update_apply, if_neg h]

Premises used: Polynomial.coeff_update_apply, if_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : ∀ (n_1 : ℕ), (p.update n 0).coeff n_1 = (erase n p).coeff n_1
⊢ p.update n 0 = erase n p

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
a : (if n_1 = n then 0 else p.coeff n_1) = (erase n p).coeff n_1
a₁ a₂ : (if n_1 = n then 0 else p.coeff n_1) = if n_1 = n then 0 else p.coeff n_1
⊢ (p.update n 0).coeff n_1 = (erase n p).coeff n_1

Tactic:
rw [coeff_update_apply, coeff_erase]

Premises used: Polynomial.coeff_erase, Polynomial.coeff_update_apply
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
inst_1 : Decidable (a = 0)
simp :
  (if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support) =
    if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
simp only [support, update, Finsupp.support_update, AddMonoidAlgebra.update, ofCoeff,
      AddMonoidAlgebra.coeff]

Premises used: Polynomial.update, AddMonoidAlgebra.coeff, Finsupp.support_update, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.update, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ (if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support) =
    if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
inst_1 : Decidable (a = 0)
simp :
  (if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support) =
    if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
classical
    simp only [support, update, Finsupp.support_update, AddMonoidAlgebra.update, ofCoeff,
      AddMonoidAlgebra.coeff]
    congr

Premises used: Polynomial.update, AddMonoidAlgebra.coeff, Finsupp.support_update, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.update, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : (erase n p).support = p.support.erase n
rw₁ rw₂ : p.support.erase n = p.support.erase n
⊢ (p.update n 0).support = p.support.erase n

Tactic:
rw [update_zero_eq_erase, support_erase]

Premises used: Polynomial.update_zero_eq_erase, Polynomial.support_erase