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

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ q.coeff.support, b ≠ aq → (if ap + b = ap + aq then p.coeff ap * q.coeff b else 0) = 0

pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ aq ∉ q.coeff.support → (if ap + aq = ap + aq then p.coeff ap * q.coeff aq else 0) = 0

pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
·

Goal state after:
case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ q.coeff.support, b ≠ aq → (if ap + b = ap + aq then p.coeff ap * q.coeff b else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
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 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
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
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 neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ ((monomial n) a).leadingCoeff = a

pp: case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
·

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
·

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ b ∈ antidiagonal (p.natDegree + q.natDegree), b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0

pp: case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ b ∈ antidiagonal (p.natDegree + q.natDegree), b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ aq ∉ q.coeff.support → (if ap + aq = ap + aq then p.coeff ap * q.coeff aq else 0) = 0

pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ aq ∉ q.coeff.support → (if ap + aq = ap + aq then p.coeff ap * q.coeff aq else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
·

Goal state after:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
·

Goal state after:
case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case pos
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree

pp: case neg
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case neg
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case neg.pn
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

pp: case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
·

Goal state after:
case neg.pn
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
·

Goal state after:
case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r).coeff (Function.invFun D ⊥) = r

pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff (Function.invFun D (D a)) = r

Tactic:
·

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r).coeff (Function.invFun D ⊥) = r
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff (Function.invFun D (D a)) = r

Tactic:
·

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff (Function.invFun D (D a)) = r
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ ⊥ = 0 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0

Tactic:
·

Goal state after:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ ⊥ = 0 ∧ m = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 1 ↔ ⊥ = 0 ∧ m = 1 ∨ ⊥ = 1 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 1 ↔ ↑a✝ = 0 ∧ m = 1 ∨ ↑a✝ = 1 ∧ m = 0

Tactic:
·

Goal state after:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 1 ↔ ⊥ = 0 ∧ m = 1 ∨ ⊥ = 1 ∧ m = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 1 ↔ ↑a✝ = 0 ∧ ⊥ = 1 ∨ ↑a✝ = 1 ∧ ⊥ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ ⊥ = 0 ∧ m = 2 ∨ ⊥ = 1 ∧ m = 1 ∨ ⊥ = 2 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0

Tactic:
·

Goal state after:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ ⊥ = 0 ∧ m = 2 ∨ ⊥ = 1 ∧ m = 1 ∨ ⊥ = 2 ∧ m = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 2 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 0

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔ ⊥ = 0 ∧ m = 3 ∨ ⊥ = 1 ∧ m = 2 ∨ ⊥ = 2 ∧ m = 1 ∨ ⊥ = 3 ∧ m = 0

pp: case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 3 ↔ ↑a✝ = 0 ∧ m = 3 ∨ ↑a✝ = 1 ∧ m = 2 ∨ ↑a✝ = 2 ∧ m = 1 ∨ ↑a✝ = 3 ∧ m = 0

Tactic:
·

Goal state after:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 3 ↔ ⊥ = 0 ∧ m = 3 ∨ ⊥ = 1 ∧ m = 2 ∨ ⊥ = 2 ∧ m = 1 ∨ ⊥ = 3 ∧ m = 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ n).natDegree = n * natDegree 0

pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ n).natDegree = n * natDegree 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 0

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 3 ↔ ↑a✝ = 0 ∧ ⊥ = 3 ∨ ↑a✝ = 1 ∧ ⊥ = 2 ∨ ↑a✝ = 2 ∧ ⊥ = 1 ∨ ↑a✝ = 3 ∧ ⊥ = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥

pp: case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
·

Goal state after:
case bot
h : 0 < ⊥
⊢ 1 ≤ ⊥
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
·

Goal state after:
case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
h : ⊥ < m
⊢ ⊥ + 1 ≤ m

pp: case coe
m : WithBot ℕ
a✝ : ℕ
h : ↑a✝ < m
⊢ ↑a✝ + 1 ≤ m

Tactic:
·

Goal state after:
case bot
m : WithBot ℕ
h : ⊥ < m
⊢ ⊥ + 1 ≤ m
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥

pp: case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p

pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
·

Goal state after:
case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
by rw [hp0, zero_pow hn0]; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
·

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0

pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff