awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (f i) ≠ ⊥

Tactic:
exact (this j hj hne).ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hs : s.Nonempty
hf : ∀ i ∈ s, f i ≠ 0
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
let ⟨i, hi⟩ := hs
  sum_ne_zero_of_injOn_supDegree' ⟨i, hi, hf i hi⟩ hd

Premises used: _private.0.AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree.match_1, Ne, And.intro, Exists.intro, OfNat.ofNat, AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree', Finset.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inl :
  (0 * q : (a : A) → R) (Function.invFun D (supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q)) =
    leadingCoeff D 0 * leadingCoeff D q
inr :
  ∀ (hp : p ≠ 0),
    (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ (0 * q : (a : A) → R) (Function.invFun D (supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q)) =
    leadingCoeff D 0 * leadingCoeff D q

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
inr :
  (p * 0 : (a : A) → R) (Function.invFun D (supDegree D p + supDegree.{u_1, u_3, u_5} (R := R) D 0)) =
    leadingCoeff D p * leadingCoeff D 0
inr₁ :
  ∀ (hq : q ≠ 0),
    (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ (p * 0 : (a : A) → R) (Function.invFun D (supDegree D p + supDegree.{u_1, u_3, u_5} (R := R) D 0)) =
    leadingCoeff D p * leadingCoeff D 0

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
inr :
  ∀ (ap : A) (hp : supDegree D p = D ap),
    (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
obtain ⟨ap, -, hp⟩ := exists_supDegree_mem_support D hp

Premises used: AddMonoidAlgebra.exists_supDegree_mem_support
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp_1 : p ≠ 0
hq : q ≠ 0
ap : A
hp : supDegree D p = D ap
inr :
  ∀ (aq : A) (hq : supDegree D q = D aq),
    (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq

Premises used: AddMonoidAlgebra.exists_supDegree_mem_support
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp_1 : p ≠ 0
hq_1 : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
inr :
  (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
simp_rw [leadingCoeff, hp, hq, ← hadd, Function.leftInverse_invFun hD _]

Premises used: Function.leftInverse_invFun, AddMonoidAlgebra.leadingCoeff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp_1 : p ≠ 0
hq_1 : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)

Tactic:
apply_add_of_supDegree_le hadd hD hp.le hq.le

Premises used: Eq.le, AddMonoidAlgebra.apply_add_of_supDegree_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp_1 : p ≠ 0
hq_1 : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)

Tactic:
exact apply_add_of_supDegree_le hadd hD hp.le hq.le

Premises used: Eq.le, AddMonoidAlgebra.apply_add_of_supDegree_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
hb : supDegree D p + supDegree D q ∈ Set.range D
hmem : Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).support
hmax : ∀ a ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_eq_of_max

Premises used: AddMonoidAlgebra.supDegree_eq_of_max
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
hb : supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd : A →ₙ+ B }.srange
hb₁ : ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
⊢ supDegree D p + supDegree D q ∈ Set.range D

Tactic:
rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]

Premises used: AddHom.srange_mk, SetLike.mem_coe, AddSubsemigroup.coe_set_mk, Set.range
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd : A →ₙ+ B }.srange

Tactic:
add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)

Premises used: AddMonoidAlgebra.supDegree_mem_range, AddMemClass.add_mem
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd : A →ₙ+ B }.srange

Tactic:
exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
a b : B
⊢ a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
(AddHom.srange ⟨D, hadd⟩).add_mem

Premises used: AddSubsemigroup.add_mem, Set.Mem, setOf, AddHom.srange, Set.range, AddHom.mk
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
exact (AddHom.srange ⟨D, hadd⟩).add_mem

Premises used: AddSubsemigroup.add_mem, AddHom.srange, AddHom.mk
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
hmem : leadingCoeff D p * leadingCoeff D q ≠ 0
⊢ Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).support

Tactic:
simp_rw [Finsupp.mem_support_iff, apply_supDegree_add_supDegree hD hadd]

Premises used: Finsupp.mem_support_iff, AddMonoidAlgebra.apply_supDegree_add_supDegree
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
hpq
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
exact hpq
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ AddLeftMono B

Tactic:
have := addLeftMono_of_addLeftStrictMono B
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : AddLeftMono B
⊢ AddRightMono B

Tactic:
have := addRightMono_of_addRightStrictMono B
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this_1 : AddLeftMono B
this : AddRightMono B
⊢ ∀ a ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q

Tactic:
fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

Premises used: AddMonoidAlgebra.supDegree_mul_le, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this_1 : AddLeftMono B
this : AddRightMono B
⊢ ∀ a ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q

Tactic:
exact fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

Premises used: AddMonoidAlgebra.supDegree_mul_le, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
(hp (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
exact (hp (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h : Nontrivial R
apply : leadingCoeff D p * leadingCoeff D q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_mul hD hadd ?_ hp hq.ne_zero

Premises used: AddMonoidAlgebra.supDegree_mul, AddMonoidAlgebra.Monic.ne_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h : Nontrivial R
simp_rw : leadingCoeff D p * 1 ≠ 0
simp_rw₁ : leadingCoeff D p ≠ 0
simp_rw₂ : ¬leadingCoeff D p = 0
simp_rw₃ : ¬p = 0
simp_rw₄ : ¬False
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Ne, mul_one, not_false_eq_true
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
(hq (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
exact (hq (Subsingleton.elim _ _)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h : Nontrivial R
apply : leadingCoeff D p * leadingCoeff D q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_mul hD hadd ?_ hp.ne_zero hq

Premises used: AddMonoidAlgebra.supDegree_mul, AddMonoidAlgebra.Monic.ne_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
h : Nontrivial R
simp_rw : 1 * leadingCoeff D q ≠ 0
simp_rw₁ : leadingCoeff D q ≠ 0
simp_rw₂ : ¬leadingCoeff D q = 0
simp_rw₃ : ¬q = 0
simp_rw₄ : ¬False
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Ne, not_false_eq_true, one_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : HAdd.hAdd (α := B) ⊥ ⊥ = ⊥
hp : Monic D p
hq : Monic D q
inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : HAdd.hAdd (α := B) ⊥ ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h : Subsingleton R
inl : supDegree D (0 * q) = supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q
inl₁ :
  supDegree D (HMul.hMul (α := R[A]) 0 0) =
    supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree.{u_1, u_3, u_5} (R := R) D 0
inl₂ :
  supDegree.{u_1, u_3, u_5} (R := R) D 0 =
    supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree.{u_1, u_3, u_5} (R := R) D 0
inl₃ : ⊥ = HAdd.hAdd (α := B) ⊥ ⊥
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]

Premises used: AddMonoidAlgebra.supDegree_zero, MulZeroClass.mul_zero, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p q : R[A]
D : A → B
inst_3 : AddZeroClass A
inst_4 : Add B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : HAdd.hAdd (α := B) ⊥ ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
hq.supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero

Premises used: AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, AddMonoidAlgebra.Monic.ne_zero