mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
·

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
⊢ degree 0 = ↑n ↔ natDegree 0 = n

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
⊢ degree 0 = ↑n ↔ natDegree 0 = n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ p.degree ≤ q.degree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ p.degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C a).degree ≤ 0

pp: case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Tactic:
·

Goal state after:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C a).degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Tactic:
·

Goal state after:
case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ (C a).natDegree = 0

pp: case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ (C a).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ ↑p.natDegree

Tactic:
← degree_eq_natDegree

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0

Tactic:
·

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).natDegree = 0

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).natDegree = i
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0

Tactic:
·

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

pp: case neg
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m

Tactic:
exacts [Nat.zero_le _, le_rfl]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree

pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
⊢ p.natDegree < q.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)

pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)

Tactic:
·

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ φ.coeff i) → C r ∣ φ
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < ↑n

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
⊢ p.degree < ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
⊢ φ.coeff i = r * c i

pp: case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i ≠ 0
⊢ φ.coeff i = r * c i
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)

Tactic:
·

Goal state after:
case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : ¬φ.coeff i ≠ 0
⊢ φ.coeff i = r * 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ p.degree < q.degree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ max p.degree ↑n

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ max p.degree ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

pp: case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
·

Goal state after:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
·

Goal state after:
case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

pp: case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
·

Goal state after:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
·

Goal state after:
case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = (C (p.coeff 0)).coeff 0

pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = (C (p.coeff 0)).coeff 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
⊢ AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
⊢ AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f

pp: case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : ¬p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f

Tactic:
·

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
⊢ ∑ i, f (↑i) (p.coeff ↑i) = p.sum f
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).degree = q.degree

Tactic:
by
  rw [add_comm, degree_add_eq_left_of_degree_lt h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
a : R
⊢ (0 + C a).natDegree = natDegree 0

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
⊢ (p + C a).natDegree = p.natDegree

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
a : R
⊢ (0 + C a).natDegree = natDegree 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree