awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a : (↑(range n) : Set ℕ) ⊆ (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLT R n) : Set R[X])
⊢ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]) ≤ degreeLT R n

Tactic:
rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]

Premises used: Finset.coe_image, Set.image_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range n) : Set ℕ)
a : degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Set ℕ) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLT R n) : Set R[X])) k

Tactic:
apply mem_degreeLT.2

Premises used: Iff.mpr, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range n) : Set ℕ)
⊢ degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) < (↑n : WithBot ℕ)

Tactic:
lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)

Premises used: Iff.mpr, lt_of_le_of_lt, Polynomial.degree_X_pow_le, Finset.mem_range, WithBot.coe_lt_coe, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range n) : Set ℕ)
⊢ degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) < (↑n : WithBot ℕ)

Tactic:
exact lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)

Premises used: Iff.mpr, lt_of_le_of_lt, Polynomial.degree_X_pow_le, Finset.mem_range, WithBot.coe_lt_coe, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
h :
  ∀ (x : Fin n),
    (↑(p + q) : R[X]).coeff (↑x : ℕ) =
      HAdd.hAdd (α := Fin n → R) (β := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
        (fun (n_1 : Fin n) ↦ (↑q : R[X]).coeff (↑n_1 : ℕ)) x
⊢ (fun (n_1 : Fin n) ↦ (↑(p + q) : R[X]).coeff (↑n_1 : ℕ)) =
    HAdd.hAdd (α := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) fun (n_1 : Fin n) ↦
      (↑q : R[X]).coeff (↑n_1 : ℕ)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x : Fin n
h : ((↑p : R[X]) + (↑q : R[X])).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)
⊢ (↑(p + q) : R[X]).coeff (↑x : ℕ) =
    HAdd.hAdd (α := Fin n → R) (β := Fin n → R) (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      (fun (n_1 : Fin n) ↦ (↑q : R[X]).coeff (↑n_1 : ℕ)) x

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p q : ↥(degreeLT R n)
x : Fin n
h h₁ : (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)
⊢ ((↑p : R[X]) + (↑q : R[X])).coeff (↑x : ℕ) = (↑p : R[X]).coeff (↑x : ℕ) + (↑q : R[X]).coeff (↑x : ℕ)

Tactic:
rw [coeff_add]

Premises used: Polynomial.coeff_add
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
h :
  ∀ (x_1 : Fin n),
    (↑(x • p) : R[X]).coeff (↑x_1 : ℕ) =
      HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R)
        (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) x_1
⊢ (fun (n_1 : Fin n) ↦ (↑(x • p) : R[X]).coeff (↑n_1 : ℕ)) =
    HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R) fun (n_1 : Fin n) ↦
      (↑p : R[X]).coeff (↑n_1 : ℕ)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x_1 : Fin n
h : (x • (↑p : R[X])).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)
⊢ (↑(x • p) : R[X]).coeff (↑x_1 : ℕ) =
    HSMul.hSMul (α := R) (β := Fin n → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ)) x_1

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x_1 : Fin n
h : x • (↑p : R[X]).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)
⊢ (x • (↑p : R[X])).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)

Tactic:
rw [coeff_smul]

Premises used: Polynomial.coeff_smul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
x : R
p : ↥(degreeLT R n)
x_1 : Fin n
⊢ x • (↑p : R[X]).coeff (↑x_1 : ℕ) = x * (↑p : R[X]).coeff (↑x_1 : ℕ)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
a :
  (↑((fun (f : Fin n → R) ↦
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
                (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
              ↥(degreeLT R n)))
          ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])
⊢ (fun (f : Fin n → R) ↦
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
            (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
          ↥(degreeLT R n)))
      ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp)) =
    Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp

Tactic:
ext1
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
a : ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
⊢ (↑((fun (f : Fin n → R) ↦
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
                (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
              ↥(degreeLT R n)))
          ((fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) : R[X])

Tactic:
simp only
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
pos : ∀ (hp0 : p = 0), ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
neg : ∀ (hp0 : ¬p = 0), ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
hp0 : p = 0
pos :
  ∀ (hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) 0),
    Eq.{u_2 + 1} (α := R[X]) (∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (coeff 0 (↑x : ℕ))) 0
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p

Tactic:
subst hp0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) 0
⊢ Eq.{u_2 + 1} (α := R[X]) (∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (coeff 0 (↑x : ℕ))) 0

Tactic:
simp only [coeff_zero, map_zero, Finset.sum_const_zero]

Premises used: map_zero, Finset.sum_const_zero, Polynomial.coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
hp0 : ¬p = 0
⊢ p.natDegree < n

Tactic:
rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
hp0 : ¬p = 0
hp₁ : p.natDegree < n
⊢ ¬p = 0

Tactic:
rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : p.natDegree < n
hp0 : ¬p = 0
rw : ∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (p.coeff (↑i : ℕ))
| p

Tactic:
rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.as_sum_range'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
p : R[X]
hp : p.natDegree < n
hp0 : ¬p = 0
conv_rhs : ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p
neg :
  Eq.{u_2 + 1} (α := R[X]) (∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)))
    (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (p.coeff (↑i : ℕ)))
⊢ ∑ x : Fin n, (monomial (↑x : ℕ) : (a : R) → R[X]) (p.coeff (↑x : ℕ)) = p

Tactic:
conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.as_sum_range'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
h :
  ∀ (i : Fin n),
    (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
        ((fun (f : Fin n → R) ↦
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
                (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
              ↥(degreeLT R n)))
          f)
        i =
      f i
⊢ (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      ((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
            ↥(degreeLT R n)))
        f) =
    f

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
h : ∑ b : Fin n, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ) = f i
⊢ (fun (p : ↥(degreeLT R n)) (n_1 : Fin n) ↦ (↑p : R[X]).coeff (↑n_1 : ℕ))
      ((fun (f : Fin n → R) ↦
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x)
              (∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) ⋯ :
            ↥(degreeLT R n)))
        f)
      i =
    f i

Tactic:
simp only [finsetSum_coeff]

Premises used: Polynomial.finsetSum_coeff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
h :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) univ b →
      b ≠ i → Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ)) 0
h₁ : i ∉ univ → Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) (↑i : ℕ)) 0
⊢ ∑ b : Fin n, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (f b)) (↑i : ℕ) = f i

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

Premises used: Polynomial.coeff_monomial, if_pos, Finset.sum_eq_single, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i j : Fin n
hji : j ≠ i
h : ¬(↑j : ℕ) = (↑i : ℕ)
⊢ Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑j : ℕ) : (a : R) → R[X]) (f j)) (↑i : ℕ)) 0

Tactic:
rw [coeff_monomial, if_neg]

Premises used: Polynomial.coeff_monomial, if_neg
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i j : Fin n
hji : j ≠ i
h h₁ h₂ h₃ : ¬j = i
⊢ ¬(↑j : ℕ) = (↑i : ℕ)

Tactic:
rwa [← Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
h : i ∉ univ
⊢ Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) (↑i : ℕ)) 0

Tactic:
(h (Finset.mem_univ _)).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
inst : Semiring R_1
R : Type u_2
inst_1 : Semiring R
n : ℕ
f : Fin n → R
i : Fin n
h : i ∉ univ
⊢ Eq.{u_2 + 1} (α := R) (coeff ((monomial (↑i : ℕ) : (a : R) → R[X]) (f i)) (↑i : ℕ)) 0

Tactic:
exact (h (Finset.mem_univ _)).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ Eq (α := Fin n → R)
      ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) :
        Fin n → R)
      (0 : Fin n → R) ↔
    p = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
x : R
simp_rw :
  Eq (α := R) (p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
    (∑ i : Fin n,
      HMul.hMul (α := R)
        ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) i :
          R)
        (x ^ (↑i : ℕ)))
⊢ eval x p =
    ∑ i : Fin n,
      HMul.hMul (α := R)
        ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) i :
          R)
        (x ^ (↑i : ℕ))

Tactic:
simp_rw [eval_eq_sum]

Premises used: Polynomial.eval_eq_sum
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
x : R
simp_rw : ∀ (i : ℕ), True
⊢ ∀ (i : ℕ), 0 * x ^ i = 0

Tactic:
simp_rw [zero_mul, forall_const]

Premises used: MulZeroClass.zero_mul, forall_const
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
x : R
⊢ Eq (α := R) (p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
    (∑ i : Fin n,
      HMul.hMul (α := R)
        ((degreeLTEquiv R n : (a : ↥(degreeLT R n)) → Fin n → R)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) x) p hp) i :
          R)
        (x ^ (↑i : ℕ)))

Tactic:
exact (sum_fin _ (by simp_rw [zero_mul, forall_const]) (mem_degreeLT.mp hp)).symm

Premises used: Polynomial.sum_fin, Iff.mp, Eq.symm, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
h :
  ∀ (x : R[X]),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
      Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
⊢ Eq (α := Submodule R R[X]) (degreeLT R (n + 1)) (degreeLE R (↑n : WithBot ℕ))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
pos :
  ∀ (x_zero : x = 0),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
      Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
neg :
  ∀ (x_zero : ¬x = 0),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
      Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x

Tactic:
by_cases x_zero : x = 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
pos :
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) 0 ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x

Tactic:
simp_rw [x_zero, Submodule.zero_mem]

Premises used: Submodule.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero rwa rwa₁ rwa₂ rwa₃ : ¬x = 0
⊢ x ≠ 0

Tactic:
rwa [ne_eq]

Premises used: ne_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
neg : x.degree < (↑(n + 1) : WithBot ℕ) ↔ Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x
neg₁ : x.degree < (↑(n + 1) : WithBot ℕ) ↔ x.degree ≤ (↑n : WithBot ℕ)
neg₂ : x.natDegree < n + 1 ↔ x.degree ≤ (↑n : WithBot ℕ)
neg₃ : x.natDegree < n + 1 ↔ x.natDegree ≤ n
neg₄ neg₅ : x.natDegree ≤ n ↔ x.natDegree ≤ n
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (n + 1)) x ↔
    Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) x

Tactic:
rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]

Premises used: Polynomial.natDegree_lt_iff_degree_lt, Nat.lt_succ_iff, Polynomial.mem_degreeLE, Polynomial.natDegree_le_iff_degree_le, Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : { p : R[X] // p.Monic ∧ p.natDegree = n }
rcases :
  ∀ (p : R[X]) (hp : p.Monic),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree)
      (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯) : R[X]).eraseLead
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) (↑p : R[X]).eraseLead

Tactic:
rcases p with ⟨p, hp, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
simp : p.eraseLead.degree < (↑p.natDegree : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree)
    (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯) : R[X]).eraseLead

Tactic:
simp only [mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p.eraseLead.degree < (↑p.natDegree : WithBot ℕ)

Tactic:
lt_of_lt_of_le ?_ degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
refine : p.eraseLead.degree < p.degree
⊢ p.eraseLead.degree < (↑p.natDegree : WithBot ℕ)

Tactic:
refine lt_of_lt_of_le ?_ degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p.eraseLead.degree < p.degree

Tactic:
degree_eraseLead_lt (Polynomial.Monic.ne_zero_of_polynomial_ne hp one_ne_zero)

Premises used: Polynomial.Monic.ne_zero_of_polynomial_ne, Polynomial.degree_eraseLead_lt, one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p.eraseLead.degree < p.degree

Tactic:
exact degree_eraseLead_lt (Polynomial.Monic.ne_zero_of_polynomial_ne hp one_ne_zero)

Premises used: Polynomial.Monic.ne_zero_of_polynomial_ne, Polynomial.degree_eraseLead_lt, one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
rw : (HPow.hPow (α := R[X]) X n).natDegree = n
rw₁ : (↑p : R[X]).degree < (HPow.hPow (α := R[X]) X n).degree
⊢ (HPow.hPow (α := R[X]) X n + (↑p : R[X])).natDegree = n

Tactic:
rw [natDegree_add_eq_left_of_degree_lt]

Premises used: Polynomial.natDegree_add_eq_left_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (HPow.hPow (α := R[X]) X n).natDegree = n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p : R[X]).degree < (HPow.hPow (α := R[X]) X n).degree

Tactic:
simp [mem_degreeLT.1 p.2]

Premises used: Iff.mp, Polynomial.mem_degreeLT, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
a :
  (↑((fun (p_1 : ↥(degreeLT R p.natDegree)) ↦
            (Subtype.mk (p := fun (p_2 : R[X]) ↦ p_2.Monic ∧ p_2.natDegree = p.natDegree)
                (HPow.hPow (α := R[X]) X p.natDegree + (↑p_1 : R[X])) ⋯ :
              { p_2 : R[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }))
          ((fun (p_1 : { p_1 : R[X] // p_1.Monic ∧ p_1.natDegree = p.natDegree }) ↦
              Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) x)
                (↑p_1 : R[X]).eraseLead ⋯)
            (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯))) :
      R[X]) =
    (↑(Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯) : R[X])
⊢ Eq (α := { p_1 : R[X] // p_1.Monic ∧ p_1.natDegree = p.natDegree })
    ((fun (p_1 : ↥(degreeLT R p.natDegree)) ↦
        (Subtype.mk (p := fun (p_2 : R[X]) ↦ p_2.Monic ∧ p_2.natDegree = p.natDegree)
            (HPow.hPow (α := R[X]) X p.natDegree + (↑p_1 : R[X])) ⋯ :
          { p_2 : R[X] // p_2.Monic ∧ p_2.natDegree = p.natDegree }))
      ((fun (p_1 : { p_1 : R[X] // p_1.Monic ∧ p_1.natDegree = p.natDegree }) ↦
          Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R p.natDegree) x)
            (↑p_1 : R[X]).eraseLead ⋯)
        (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯)))
    (Subtype.mk (p := fun (p_1 : R[X]) ↦ p_1.Monic ∧ p_1.natDegree = p.natDegree) p ⋯)

Tactic:
ext1