mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ ∀ (i : Fin (n + 1)), Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

pp: case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i

Tactic:
·

Goal state after:
case succ.refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ ∀ (i : Fin (n + 1)), Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree ≤ s.sup fun i ↦ (f i).natDegree

pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).natDegree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree

Tactic:
·

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree ≤ s.sup fun i ↦ (f i).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).natDegree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree

Tactic:
·

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).natDegree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
·

Goal state after:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case pos
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).natDegree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree

pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (f i).natDegree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).natDegree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i ≠ 0

Tactic:
Function.extend_apply' _ _ _ hi,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ f.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
·

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree ≤ p.degree

pp: case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map (natDegree ∘ fun x ↦ X - C x) s).sum = s.card

pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic

Tactic:
·

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map (natDegree ∘ fun x ↦ X - C x) s).sum = s.card
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ (k • p).natDegree = p.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).natDegree = p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ (k • p).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic

Tactic:
·

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i

Tactic:
·

Goal state after:
case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 → q = 0

pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 → q = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Tactic:
· rintro rfl
    simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 → q = 0

pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 → q = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLE R ↑n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1))) ≤ degreeLE R ↑n

Tactic:
·

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLE R ↑n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n)) ≤ degreeLT R n

Tactic:
·

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ span R (p * q) ≤ Subalgebra.toSubmodule (adjoin R (s ∪ t))

pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)

Tactic:
·

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ span R (p * q) ≤ Subalgebra.toSubmodule (adjoin R (s ∪ t))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1.refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)

pp: case refine_1.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ adjoin R (s ∪ t)

Tactic:
·

Goal state after:
case refine_1.refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 1
⊢ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 1
⊢ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 2
⊢ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 2
⊢ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n).natDegree = n

pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p).degree < (X ^ n).degree

Tactic:
·

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n).natDegree = n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p).degree < (X ^ n).degree

Tactic:
·

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p).degree < (X ^ n).degree
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)

Tactic:
·

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (X ^ n).eraseLead + p = p

pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p.degree < (X ^ n).degree

Tactic:
·

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (X ^ n).eraseLead + p = p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p.degree < (X ^ n).degree

Tactic:
·

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p.degree < (X ^ n).degree