awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
simp : Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R) (∑ x ∈ range n, if i = x then (↑(n.choose (x + 1)) : R) else 0)
⊢ Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R)
    (coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i)

Tactic:
simp only [finsetSum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]

Premises used: Polynomial.C_eq_natCast, Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
h₀ : ∀ b ∈ range n, b ≠ i → Eq.{u + 1} (α := R) (if i = b then (↑(n.choose (b + 1)) : R) else 0) 0
h₁ : i ∉ range n → Eq.{u + 1} (α := R) (if i = i then (↑(n.choose (i + 1)) : R) else 0) 0
⊢ Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R) (∑ x ∈ range n, if i = x then (↑(n.choose (x + 1)) : R) else 0)

Tactic:
rw [Finset.sum_eq_single i, if_pos rfl]

Premises used: if_pos, Finset.sum_eq_single, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → Eq.{u + 1} (α := R) (if i = b then (↑(n.choose (b + 1)) : R) else 0) 0

Tactic:
simp +contextual only [@eq_comm _ i, if_false,
        imp_true_iff]

Premises used: if_false, eq_comm, imp_true_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ i ∉ range n → Eq.{u + 1} (α := R) (if i = i then (↑(n.choose (i + 1)) : R) else 0) 0

Tactic:
simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt,
        Nat.cast_zero, Finset.mem_range, not_lt, if_true, imp_true_iff]

Premises used: if_true, Nat.lt_add_one_iff, Finset.mem_range, imp_true_iff, not_lt, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
i : ℕ
⊢ (comp 0 (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑0 : R)

Tactic:
simp only [zero_comp, coeff_zero, Nat.cast_zero]

Premises used: Polynomial.zero_comp, Polynomial.coeff_zero, Nat.cast_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih :
  ∀ (i : ℕ),
    (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
i : ℕ
⊢ (comp (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    (↑((n + 1).choose (i + 1)) : R)

Tactic:
simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]

Premises used: Nat.choose_succ_succ, Polynomial.coeff_add, geom_sum_succ', Nat.cast_add, Polynomial.add_comp, Polynomial.coeff_X_add_one_pow, Polynomial.X_pow_comp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n i : ℕ
zero :
  ∀ (i : ℕ),
    (comp (∑ i ∈ range 0, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
      (↑(Nat.choose 0 (i + 1)) : R)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (i : ℕ),
        (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
          (↑(n.choose (i + 1)) : R))
    (i : ℕ),
    (comp (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
      (↑((n + 1).choose (i + 1)) : R)
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)

Tactic:
induction n generalizing i with
  | zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  | succ n ih =>
    simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]

Premises used: Polynomial.zero_comp, Nat.choose_succ_succ, Polynomial.coeff_add, geom_sum_succ', Nat.cast_add, Polynomial.add_comp, Polynomial.coeff_X_add_one_pow, Polynomial.coeff_zero, Nat.cast_zero, Polynomial.X_pow_comp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
n : ℕ
hn : n ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
n : ℕ
hn : n ≠ 0
h : Nontrivial R
obtain : ∀ (n : ℕ) (hn : n.succ ≠ 0), Monic.{u} (R := R) (∑ i ∈ range n.succ, P ^ i)
⊢ Monic.{u} (R := R) (∑ i ∈ range n, P ^ i)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
rw : (P ^ n + ∑ i ∈ range n, P ^ i).Monic
⊢ Monic.{u} (R := R) (∑ i ∈ range n.succ, P ^ i)

Tactic:
rw [geom_sum_succ']

Premises used: geom_sum_succ'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ (P ^ n + ∑ i ∈ range n, P ^ i).Monic

Tactic:
(hP.pow _).add_of_left ?_

Premises used: Polynomial.Monic.add_of_left, Polynomial.Monic.pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
refine : degree.{u} (R := R) (∑ i ∈ range n, P ^ i) < (P ^ n).degree
⊢ (P ^ n + ∑ i ∈ range n, P ^ i).Monic

Tactic:
refine (hP.pow _).add_of_left ?_

Premises used: Polynomial.Monic.add_of_left, Polynomial.Monic.pow
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ degree.{u} (R := R) (∑ i ∈ range n, P ^ i) < (P ^ n).degree

Tactic:
lt_of_le_of_lt (degree_sum_le _ _) ?_

Premises used: lt_of_le_of_lt, Polynomial.degree_sum_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
refine : ((range n).sup fun (b : ℕ) ↦ (P ^ b).degree) < (P ^ n).degree
⊢ degree.{u} (R := R) (∑ i ∈ range n, P ^ i) < (P ^ n).degree

Tactic:
refine lt_of_le_of_lt (degree_sum_le _ _) ?_

Premises used: lt_of_le_of_lt, Polynomial.degree_sum_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
rw : ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree
rw₁ : ⊥ < (P ^ n).degree
⊢ ((range n).sup fun (b : ℕ) ↦ (P ^ b).degree) < (P ^ n).degree

Tactic:
rw [Finset.sup_lt_iff]

Premises used: Finset.sup_lt_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
simp : ∀ b < n, LT.lt (α := WithBot ℕ) (↑(P ^ b).natDegree : WithBot ℕ) (↑(P ^ n).natDegree : WithBot ℕ)
⊢ ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree

Tactic:
simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]

Premises used: Polynomial.degree_eq_natDegree, Finset.mem_range, Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
simp : ∀ b < n, b * P.natDegree < n * P.natDegree
⊢ ∀ b < n, LT.lt (α := WithBot ℕ) (↑(P ^ b).natDegree : WithBot ℕ) (↑(P ^ n).natDegree : WithBot ℕ)

Tactic:
simp only [Nat.cast_lt, hP.natDegree_pow]

Premises used: Polynomial.Monic.natDegree_pow, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
k : ℕ
⊢ k < n → k * P.natDegree < n * P.natDegree

Tactic:
nsmul_lt_nsmul_left hdeg

Premises used: nsmul_lt_nsmul_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
k : ℕ
⊢ k < n → k * P.natDegree < n * P.natDegree

Tactic:
exact nsmul_lt_nsmul_left hdeg

Premises used: nsmul_lt_nsmul_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
rw : ¬P ^ n = 0
⊢ ⊥ < (P ^ n).degree

Tactic:
rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]

Premises used: bot_lt_iff_ne_bot, Ne, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ¬P ^ n = 0

Tactic:
(hP.pow _).ne_zero

Premises used: Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ¬P ^ n = 0

Tactic:
exact (hP.pow _).ne_zero

Premises used: Polynomial.Monic.pow, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.degree
n : ℕ
hn : n ≠ 0
⊢ Monic.{u} (R := R) (∑ i ∈ range n, P ^ i)

Tactic:
hP.geom_sum (natDegree_pos_iff_degree_pos.2 hdeg) hn

Premises used: Iff.mpr, Polynomial.Monic.geom_sum, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
h : Nontrivial R
apply : 0 < natDegree.{u} (R := R) X
⊢ Monic.{u} (R := R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
apply monic_X.geom_sum _ hn

Premises used: Polynomial.Monic.geom_sum, Polynomial.monic_X
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
h : Nontrivial R
⊢ 0 < natDegree.{u} (R := R) X

Tactic:
simp only [natDegree_X, zero_lt_one]

Premises used: Polynomial.natDegree_X, zero_lt_one
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
simp :
  (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n

Tactic:
simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]

Premises used: Finset.sum_ite_eq', Polynomial.restriction, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, ite_not
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
neg :
  ∀ (h : ¬p.coeff n = 0),
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
        R) =
      p.coeff n
⊢ (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
pos : Eq.{u + 1} (α := R) (↑0 : R) 0
⊢ (↑0 : R) = p.coeff n

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ Eq.{u + 1} (α := R) (↑0 : R) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x) (p.coeff n)
          ⋯) :
      R) =
    p.coeff n

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
simp :
  (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
neg neg₁ :
  ∀ (h : ¬p.coeff n = 0),
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
        R) =
      p.coeff n
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n

Tactic:
classical
  simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

Premises used: Finset.sum_ite_eq', Polynomial.restriction, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, ite_not
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
h : ∀ (i : ℕ), i ∈ p.restriction.support ↔ i ∈ p.support
⊢ p.restriction.support = p.support

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
h : p.restriction.coeff i = 0 ↔ p.coeff i = 0
⊢ i ∈ p.restriction.support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Premises used: not_iff_not, Polynomial.mem_support_iff, Ne
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
rw : (↑(p.restriction.coeff i) : R) = 0
| p.coeff i = 0

Tactic:
rw [← coeff_restriction]

Premises used: Polynomial.coeff_restriction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
h : p.restriction.coeff i = 0 ↔ (↑(p.restriction.coeff i) : R) = 0
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0

Tactic:
conv_rhs => rw [← coeff_restriction]

Premises used: Polynomial.coeff_restriction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
rw : Eq.{u + 1} (α := R) (↑0 : R) 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ (↑(p.restriction.coeff i) : R) = 0

Tactic:
rw [H, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ (↑(p.restriction.coeff i) : R) = 0

Tactic:
exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
n : ℕ
rw :
  (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R : (a : ↥(Subring.closure (↑p.coeffs : Set R))) → R)
      (p.restriction.coeff n) =
    p.coeff n
rw₁ : (↑(p.restriction.coeff n) : R) = p.coeff n
rw₂ rw₃ : p.coeff n = p.coeff n
⊢ coeff (map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) n = p.coeff n

Tactic:
rw [coeff_map, Algebra.algebraMap_ofSubsemiring_apply, coeff_restriction]

Premises used: Algebra.algebraMap_ofSubsemiring_apply, Polynomial.coeff_map, Polynomial.coeff_restriction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.degree = p.degree

Tactic:
simp [degree]

Premises used: Polynomial.degree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.natDegree = p.natDegree

Tactic:
simp [natDegree]

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
simp : p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1
⊢ p.restriction.Monic ↔ p.Monic

Tactic:
simp only [Monic, leadingCoeff, natDegree_restriction]

Premises used: Polynomial.leadingCoeff, Polynomial.Monic, Polynomial.natDegree_restriction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : p.restriction.coeff p.natDegree = 1 ↔ (↑(p.restriction.coeff p.natDegree) : R) = 1
⊢ p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1

Tactic:
rw [← @coeff_restriction _ _ p]

Premises used: Polynomial.coeff_restriction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
rw : Eq.{u + 1} (α := R) (↑1 : R) 1
rw₁ rw₂ : Eq.{u + 1} (α := R) 1 1
⊢ (↑(p.restriction.coeff p.natDegree) : R) = 1

Tactic:
rw [H, OneMemClass.coe_one]

Premises used: OneMemClass.coe_one
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ (↑(p.restriction.coeff p.natDegree) : R) = 1

Tactic:
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
⊢ Eq.{u + 1} (α := (↥(Subring.closure (↑(coeffs 0) : Set R)))[X]) (restriction 0) 0

Tactic:
simp only [restriction, Finset.sum_empty, support_zero]

Premises used: Polynomial.restriction, Finset.sum_empty, Polynomial.support_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
i : ℕ
rw : Eq.{u + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
⊢ Eq.{u + 1} (α := R) (↑(coeff (restriction 1) i) : R) (↑(coeff 1 i) : R)

Tactic:
rw [coeff_restriction', coeff_one, coeff_one]

Premises used: Polynomial.coeff_one, Polynomial.coeff_restriction'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
i : ℕ
pos : i = 0 → Eq.{u + 1} (α := R) 1 (↑1 : R)
neg : ¬i = 0 → Eq.{u + 1} (α := R) 0 (↑0 : R)
⊢ Eq.{u + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
i : ℕ
h : i = 0
⊢ Eq.{u + 1} (α := R) 1 (↑1 : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
i : ℕ
h : ¬i = 0
⊢ Eq.{u + 1} (α := R) 0 (↑0 : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Ring R
inst_1 : Semiring S
f : R →+* S
x : S
p : R[X]
⊢ eval₂ f x p = eval₂ (f.comp (Subring.subtype (Subring.closure (↑p.coeffs : Set R)))) x p.restriction

Tactic:
simp only [eval₂_eq_sum, sum, support_restriction, ← @coeff_restriction _ _ p, RingHom.comp_apply,
    Subring.coe_subtype]

Premises used: Subring.coe_subtype, Polynomial.sum, Polynomial.coeff_restriction, RingHom.comp_apply, Polynomial.support_restriction, Polynomial.eval₂_eq_sum
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) x ∈ I.carrier
⊢ c • x ∈ I.carrier

Tactic:
rw [← C_mul']

Premises used: Polynomial.C_mul'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) x ∈ I.carrier

Tactic:
I.mul_mem_left _ H

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) x ∈ I.carrier

Tactic:
exact I.mul_mem_left _ H

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
I : Ideal R[X]
x : R[X]
⊢ x ∈ I.ofPolynomial ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
p : R[X]
hp : ∀ (n : ℕ), Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (p.coeff n)
⊢ p ∈ I

Tactic:
sum_C_mul_X_pow_eq p ▸ Submodule.sum_mem I fun n _ => I.mul_mem_right _ (hp n)

Premises used: Submodule.sum_mem, Polynomial.sum_C_mul_X_pow_eq, Eq.rec, HPow.hPow, Ideal.mul_mem_right, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
mp : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f → ∀ (n : ℕ), f.coeff n ∈ I
mpr : (∀ (n : ℕ), f.coeff n ∈ I) → Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f ↔ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hf

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
mp : ∀ (x : R[X]) (h : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) x) (n : ℕ), x.coeff n ∈ I
mp₁ : ∀ (n : ℕ), coeff 0 n ∈ I
mp₂ :
  ∀ (x y : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x)
    (hy : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) y),
    (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I
mp₃ :
  ∀ (a x : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x),
    (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
mp : ∀ (x : R) (hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f), f.coeff n ∈ I
⊢ f.coeff n ∈ I

Tactic:
obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
mp : (if n = 0 then x else 0) ∈ I
⊢ f.coeff n ∈ I

Tactic:
rw [← hx.right, coeff_C]

Premises used: Polynomial.coeff_C, And.right
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
pos : ∀ (h : n = 0), (if n = 0 then x else 0) ∈ I
neg : ∀ (h : ¬n = 0), (if n = 0 then x else 0) ∈ I
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
by_cases h : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
simpa [h] using hx.left

Premises used: And.left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

Tactic:
simp