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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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.support
hne : a ≠ aq
he : D ap + D a = D ap + D aq
⊢ False

Tactic:
(add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he

Premises used: Iff.mpr, add_lt_add_right, Function.Injective.ne_iff, LE.le.lt_of_ne, LE.le.trans, LT.lt.ne, 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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.support
hne : a ≠ aq
he : D ap + D a = D ap + D aq
⊢ False

Tactic:
exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he

Premises used: Iff.mpr, add_lt_add_right, Function.Injective.ne_iff, LE.le.lt_of_ne, LE.le.trans, LT.lt.ne, 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : aq ∉ q.support
h₁ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) = 0
h₂ : HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) (0 : R) = 0
h₃ h₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R) else 0) =
    0

Tactic:
rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]

Premises used: Finsupp.notMem_support_iff, if_pos, MulZeroClass.mul_zero, Iff.mp, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0

Tactic:
fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h₀ : ∀ (a : A) (ha : a ∈ p.support) (hne : a ≠ ap) (a' : A) (ha' : a' ∈ q.support) (he : a + a' = ap + aq), False
⊢ ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0

Tactic:
refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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 ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : a + a' = ap + aq
⊢ D (a + a') = D (ap + aq)

Tactic:
apply_fun D at he
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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 ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D (a + a') = D (ap + aq)
⊢ D a + D a' = D ap + D aq

Tactic:
simp_rw [hadd] at he
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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 ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D a + D a' = D ap + D aq
⊢ 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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 ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D a + D a' = D ap + D aq
this : AddLeftMono B
⊢ False

Tactic:
(add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he

Premises used: Iff.mpr, Function.Injective.ne_iff, LE.le.lt_of_ne, add_lt_add_of_lt_of_le, LE.le.trans, LT.lt.ne, 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : 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 ∈ p.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.support
he : D a + D a' = D ap + D aq
this : AddLeftMono B
⊢ False

Tactic:
exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he

Premises used: Iff.mpr, Function.Injective.ne_iff, LE.le.lt_of_ne, add_lt_add_of_lt_of_le, LE.le.trans, LT.lt.ne, 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0

Tactic:
fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)

Premises used: Iff.mpr, Finset.sum_eq_zero, ite_eq_right_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h₁ :
  ∀ (h : ap ∉ p.support),
    ∀ a ∈ q.support,
      ap + a = ap + aq → HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) a : R) = 0
⊢ ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0

Tactic:
refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)

Premises used: Iff.mpr, Finset.sum_eq_zero, ite_eq_right_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h : ap ∉ p.support
a : A
h_1 : a ∈ q.support
h_2 : ap + a = ap + aq
h₁ : HMul.hMul (α := R) (β := R) (0 : R) ((q : (a : A) → R) a : R) = 0
h₂ h₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) a : R) = 0

Tactic:
rw [Finsupp.notMem_support_iff.mp h, zero_mul]

Premises used: Finsupp.notMem_support_iff, MulZeroClass.zero_mul, Iff.mp
-- 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
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
rw : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
⊢ leadingCoeff D (single a r) = r

Tactic:
rw [leadingCoeff, supDegree_single]

Premises used: AddMonoidAlgebra.supDegree_single, 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
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
neg : ∀ (hr : ¬r = 0), (single a r : (a : A) → R) (Function.invFun D (D a)) = r
⊢ (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r

Tactic:
split_ifs with hr
-- 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
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r : (a : A) → R) (Function.invFun D ⊥) = r

Tactic:
simp [hr]
-- 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
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
neg : (single a r : (a : A) → R) a = r
neg₁ : (if a = a then r else 0) = r
neg₂ neg₃ : r = r
⊢ (single a r : (a : A) → R) (Function.invFun D (D a)) = r

Tactic:
rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]

Premises used: AddMonoidAlgebra.single_apply, if_pos, Function.leftInverse_invFun, 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
D : A → B
inst_3 : Nonempty A
hD : Function.Injective D
a : A
r : R
rw : (single a r : (a : A) → R) (Function.invFun D (supDegree D (single a r))) = r
rw₁ rw₂ rw₃ : (single a r : (a : A) → R) (Function.invFun D (if r = 0 then ⊥ else D a)) = r
pos : ∀ (hr : r = 0), (single a r : (a : A) → R) (Function.invFun D ⊥) = r
neg neg₁ : ∀ (hr : ¬r = 0), (single a r : (a : A) → R) (Function.invFun D (D a)) = r
⊢ leadingCoeff D (single a r) = r

Tactic:
classical
  rw [leadingCoeff, supDegree_single]
  split_ifs with hr
  · simp [hr]
  · rw [Function.leftInverse_invFun hD, single_apply, if_pos rfl]

Premises used: AddMonoidAlgebra.supDegree_single, AddMonoidAlgebra.single_apply, if_pos, Function.leftInverse_invFun, AddMonoidAlgebra.leadingCoeff, 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
D : A → B
inst_3 : Nonempty A
⊢ Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 0

Tactic:
rfl

Premises used: AddMonoidAlgebra.leadingCoeff, 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 : Nonempty A
inst_4 : Nontrivial R
hp : Monic D p
h : p = 0
simp_rw : False
simp_rw₁ : ∀ (hp : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 1), False
simp_rw₂ : ∀ (hp : Eq.{u_1 + 1} (α := R) 0 1), False
⊢ False

Tactic:
simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp

Premises used: zero_ne_one, AddMonoidAlgebra.leadingCoeff_zero, AddMonoidAlgebra.Monic
-- 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
inst_3 : AddZeroClass A
hD : Function.Injective D
rw : Eq.{u_1 + 1} (α := R) (leadingCoeff D 1) 1
rw₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D (single 0 1)) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Monic.{u_1, u_3, u_5} (R := R) D 1

Tactic:
rw [Monic, one_def, leadingCoeff_single hD]

Premises used: AddMonoidAlgebra.leadingCoeff_single, AddMonoidAlgebra.Monic, AddMonoidAlgebra.one_def
-- 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
hp : p ≠ 0
⊢ ∃ a ∈ p.support, supDegree D p = D a

Tactic:
Finset.exists_mem_eq_sup _ (Finsupp.support_nonempty_iff.mpr hp) D

Premises used: Iff.mpr, Finsupp.support_nonempty_iff, Finset.exists_mem_eq_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 : R[A]
D : A → B
hp : p ≠ 0
obtain : ∀ (a : A) (he : supDegree D p = D a), supDegree D p ∈ Set.range D
⊢ supDegree D p ∈ Set.range D

Tactic:
obtain ⟨a, -, he⟩ := 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 : R[A]
D : A → B
hp : p ≠ 0
a : A
he : supDegree D p = D a
⊢ supDegree D p ∈ Set.range D

Tactic:
⟨a, he.symm⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Eq.symm
-- 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
hp : p ≠ 0
a : A
he : supDegree D p = D a
⊢ supDegree D p ∈ Set.range D

Tactic:
exact ⟨a, he.symm⟩
-- 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]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) < b

Tactic:
supDegree_sum_le.trans_lt ((Finset.sup_lt_iff ?_).mpr h)

Premises used: Iff.mpr, Finset.sup_lt_iff, LE.le.trans_lt, AddMonoidAlgebra.supDegree_sum_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
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
refine : ⊥ < b
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) < b

Tactic:
refine supDegree_sum_le.trans_lt ((Finset.sup_lt_iff ?_).mpr h)

Premises used: Iff.mpr, Finset.sup_lt_iff, LE.le.trans_lt, AddMonoidAlgebra.supDegree_sum_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
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
obtain : ∀ (i : ι) (hi : i ∈ s), ⊥ < b
⊢ ⊥ < b

Tactic:
obtain ⟨i, hi⟩ := hs
-- 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]
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
i : ι
hi : i ∈ s
⊢ ⊥ < b

Tactic:
bot_le.trans_lt (h i hi)

Premises used: LE.le.trans_lt, bot_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
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
i : ι
hi : i ∈ s
⊢ ⊥ < b

Tactic:
exact bot_le.trans_lt (h i hi)

Premises used: LE.le.trans_lt, bot_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
h : supDegree D q < supDegree D p
apply : supDegree D p ≤ supDegree D (p + q)
⊢ supDegree D (p + q) = supDegree D p

Tactic:
apply (supDegree_add_le.trans <| sup_le le_rfl h.le).antisymm

Premises used: le_rfl, AddMonoidAlgebra.supDegree_add_le, LE.le.antisymm, LT.lt.le, sup_le, LE.le.trans
-- 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
h : supDegree D q < supDegree D p
obtain : ∀ (a : A) (ha : a ∈ p.support) (he : supDegree D p = D a), supDegree D p ≤ supDegree D (p + q)
⊢ supDegree D p ≤ supDegree D (p + q)

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D (ne_zero_of_not_supDegree_le h.not_ge)

Premises used: AddMonoidAlgebra.exists_supDegree_mem_support, AddMonoidAlgebra.ne_zero_of_not_supDegree_le, LT.lt.not_ge
-- 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
h : supDegree D q < supDegree D p
a : A
ha : a ∈ p.support
he : supDegree D p = D a
rw : ∀ (h : supDegree D q < D a) (ha : a ∈ p.support) (he : supDegree D p = D a), D a ≤ supDegree D (p + q)
⊢ supDegree D p ≤ supDegree D (p + q)

Tactic:
rw [he] at h ⊢
-- 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
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
hb : a ∈ (p + q).support
⊢ D a ≤ supDegree D (p + q)

Tactic:
apply Finset.le_sup

Premises used: 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
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
hb : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)
⊢ a ∈ (p + q).support

Tactic:
rw [mem_support_iff, add_apply, apply_eq_zero_of_not_le_supDegree h.not_ge, add_zero]

Premises used: Finsupp.mem_support_iff, Finsupp.add_apply, AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree, LT.lt.not_ge, add_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
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)

Tactic:
mem_support_iff.mp ha

Premises used: Finsupp.mem_support_iff, Iff.mp
-- 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
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)

Tactic:
exact mem_support_iff.mp ha

Premises used: Finsupp.mem_support_iff, Iff.mp
-- 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
h : supDegree D p < supDegree D q
rw : supDegree D (q + p) = supDegree D q
rw₁ rw₂ : supDegree D q = supDegree D q
⊢ supDegree D (p + q) = supDegree D q

Tactic:
rw [add_comm, supDegree_add_eq_left h]

Premises used: add_comm, AddMonoidAlgebra.supDegree_add_eq_left
-- 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
h : supDegree D q < supDegree D p
obtain : ∀ (a : A) (he : D a = supDegree D p), leadingCoeff D (p + q) = leadingCoeff D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_ge)

Premises used: AddMonoidAlgebra.supDegree_mem_range, AddMonoidAlgebra.ne_zero_of_not_supDegree_le, LT.lt.not_ge
-- 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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
rw : ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
rw [leadingCoeff, supDegree_add_eq_left h, Finsupp.add_apply, ← leadingCoeff,
    apply_eq_zero_of_not_le_supDegree (D := D), add_zero]

Premises used: Finsupp.add_apply, AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree, AddMonoidAlgebra.supDegree_add_eq_left, AddMonoidAlgebra.leadingCoeff, add_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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
rw : ¬supDegree D p ≤ supDegree D q
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q

Tactic:
rw [← he, Function.apply_invFun_apply (f := D), he]

Premises used: Function.apply_invFun_apply
-- 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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬supDegree D p ≤ supDegree D q

Tactic:
h.not_ge

Premises used: LT.lt.not_ge
-- 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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬supDegree D p ≤ supDegree D q

Tactic:
exact h.not_ge

Premises used: LT.lt.not_ge
-- 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
h : supDegree D p < supDegree D q
rw : leadingCoeff D (q + p) = leadingCoeff D q
rw₁ rw₂ : leadingCoeff D q = leadingCoeff D q
⊢ leadingCoeff D (p + q) = leadingCoeff D q

Tactic:
rw [add_comm, leadingCoeff_add_eq_left h]

Premises used: AddMonoidAlgebra.leadingCoeff_add_eq_left, add_comm