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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
x✝ : Multiplicative M
⊢ ((fun F ↦ F.toMulHom.comp (ofMagma R M))
        ((fun f ↦
            let __AddMonoidHom :=
              (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom;
            { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
x✝ : Multiplicative M
⊢ ((fun F ↦ F.toMulHom.comp (ofMagma R M))
        ((fun f ↦
            let __AddMonoidHom :=
              (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom;
            { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x✝ : Multiplicative M
⊢ (((fun f ↦
                let __AddMonoidHom :=
                  (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
                    coeffAddEquiv.toAddMonoidHom;
                { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
              ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F)).toMulHom.comp
        (ofMagma R M))
      x✝ =
    (F.toMulHom.comp (ofMagma R M)) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x✝ : Multiplicative M
⊢ (((fun f ↦
                let __AddMonoidHom :=
                  (liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
                    coeffAddEquiv.toAddMonoidHom;
                { toFun := (↑__AddMonoidHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ })
              ((fun F ↦ F.toMulHom.comp (ofMagma R M)) F)).toMulHom.comp
        (ofMagma R M))
      x✝ =
    (F.toMulHom.comp (ofMagma R M)) x✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : Multiplicative M →* A
x✝ : M
⊢ Additive.toMul
      ((MonoidHom.toAdditiveRight ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)))
        x✝) =
    Additive.toMul ((MonoidHom.toAdditiveRight f) x✝)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : Multiplicative M →* A
x✝ : M
⊢ Additive.toMul
      ((MonoidHom.toAdditiveRight ((fun f ↦ (↑f).comp (of R M)) ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) f)))
        x✝) =
    Additive.toMul ((MonoidHom.toAdditiveRight f) x✝)
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single_zero_right
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
F : R[M] →ₐ[R] A
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)

Tactic:
;

Goal state after:
case single_zero_right
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
F : R[M] →ₐ[R] A
m✝ : M
⊢ ((fun F ↦ liftNCAlgHom (Algebra.ofId R A) F ⋯) ((fun f ↦ (↑f).comp (of R M)) F)) (single m✝ 1) = F (single m✝ 1)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ [].prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) []).sum

Tactic:
rw [List.map_nil, Finset.sup_le_iff, List.prod_nil, List.sum_nil]

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
⊢ ∀ b ∈ (coeff 1).support, degb b ≤ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, mul_zero]
    exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A 0))) a✝¹).coeff a✝ = ((Additive.toMul 0) a✝¹).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A 0))) a✝¹).coeff a✝ = ((Additive.toMul 0) a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝¹ x✝ : AddAut M
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A (x✝¹ + x✝)))) a✝¹).coeff a✝ =
    ((Additive.toMul (Additive.ofMul (domCongr R A x✝¹) + Additive.ofMul (domCongr R A x✝))) a✝¹).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝¹ x✝ : AddAut M
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A (x✝¹ + x✝)))) a✝¹).coeff a✝ =
    ((Additive.toMul (Additive.ofMul (domCongr R A x✝¹) + Additive.ofMul (domCongr R A x✝))) a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M 1) a✝¹).coeff a✝ = (1 a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
x y : A ≃ₐ[R] A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
x y : A ≃ₐ[R] A
a✝¹ : A[M]
a✝ : M
⊢ ((mapAlgEquiv R M (x * y)) a✝¹).coeff a✝ = ((mapAlgEquiv R M x * mapAlgEquiv R M y) a✝¹).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
r : R
a✝ : Multiplicative M
⊢ ((toMultiplicative A M).toFun ((algebraMap R A[M]) r)).coeff a✝ =
    ((algebraMap R (MonoidAlgebra A (Multiplicative M))) r).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
r : R
a✝ : Multiplicative M
⊢ ((toMultiplicative A M).toFun ((algebraMap R A[M]) r)).coeff a✝ =
    ((algebraMap R (MonoidAlgebra A (Multiplicative M))) r).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
m : M
a : A
a✝ : Multiplicative M
⊢ ((toMultiplicativeAlgEquiv R A M) (single m a)).coeff a✝ = (MonoidAlgebra.single (Multiplicative.ofAdd m) a).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : AddMonoid M
m : M
a : A
a✝ : Multiplicative M
⊢ ((toMultiplicativeAlgEquiv R A M) (single m a)).coeff a✝ = (MonoidAlgebra.single (Multiplicative.ofAdd m) a).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m : M
a : A
a✝ : Additive M
⊢ ((toAdditiveAlgEquiv R A M) (single m a)).coeff a✝ = (AddMonoidAlgebra.single (Additive.ofMul m) a).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m : M
a : A
a✝ : Additive M
⊢ ((toAdditiveAlgEquiv R A M) (single m a)).coeff a✝ = (AddMonoidAlgebra.single (Additive.ofMul m) a).coeff a✝
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = some n
⊢ some n = ↑(WithBot.unbotD 0 (some n))

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = some n
⊢ some n = ↑(WithBot.unbotD 0 (some n))
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑p.natDegree = ↑n ↔ p.natDegree = n

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑p.natDegree = ↑n ↔ p.natDegree = n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
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)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).coeff.support.inf degt = (Multiset.map ((fun f ↦ f.coeff.support.inf degt) ∘ fun i ↦ f i) s.val).sum

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
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)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).coeff.support.inf degt = (Multiset.map ((fun f ↦ f.coeff.support.inf degt) ∘ fun i ↦ f i) s.val).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)

Tactic:
;

Goal state after:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (C 1).degree ≤ 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ (C 1).degree ≤ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
⊢ supDegree D (single a r) = if r = 0 then ⊥ else D a

Tactic:
by
  split_ifs with hr <;> simp [supDegree_single_ne_zero, hr]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.max = p.support.max

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.max = p.support.max
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
contrapose! hp

Goal state after:
case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ p.natDegree ≤ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
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]
h✝ : 1 = 0
⊢ ⊥ ≤ 0

pp: case neg
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]
h✝ : ¬1 = 0
⊢ D 0 ≤ 0

Tactic:
;

Goal state after:
case pos
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]
h✝ : 1 = 0
⊢ ⊥ ≤ 0

case neg
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]
h✝ : ¬1 = 0
⊢ D 0 ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)

Tactic:
have := supp_subset_range hn
  simp only [Polynomial.sum, support, coeff] at this ⊢
  exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b ↦ (f b).degree)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b ↦ (f b).degree)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 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 + q).natDegree = 0
h₁ : p.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
⊢ p.natDegree = q.natDegree

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.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 + q).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 + q).natDegree < q.natDegree
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
a : A
ha : a ∈ q.coeff.support
hne : a ≠ aq
he : D (ap + a) = D (ap + aq)
⊢ False

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
a : A
ha : a ∈ q.coeff.support
hne : a ≠ aq
he : D (ap + a) = D (ap + aq)
⊢ False
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 + q).natDegree < p.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 + q).natDegree < p.natDegree
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
h : aq ∉ q.coeff.support
⊢ (if ap + aq = ap + aq then p.coeff ap * q.coeff aq 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
h : aq ∉ q.coeff.support
⊢ (if ap + aq = ap + aq then p.coeff ap * q.coeff aq else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p = 0 → p.leadingCoeff * q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
rw [hd]

Goal state after: