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
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:
exact 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
-- 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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inl : leadingCoeff D (0 * q) = leadingCoeff D 0 * leadingCoeff D q
inr : ∀ (hp : p ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
⊢ leadingCoeff D (p * 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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inl : leadingCoeff D (0 * q) = 0 * leadingCoeff D q
inl₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 0
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0 * leadingCoeff D q

Tactic:
simp_rw [leadingCoeff_zero, zero_mul, leadingCoeff_zero]

Premises used: MulZeroClass.zero_mul, AddMonoidAlgebra.leadingCoeff_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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
inr : leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0
inr₁ : ∀ (hq : q ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
⊢ leadingCoeff D (p * 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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
inr : leadingCoeff D (p * 0) = leadingCoeff D p * 0
inr₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 0
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0

Tactic:
simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]

Premises used: AddMonoidAlgebra.leadingCoeff_zero, MulZeroClass.mul_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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
rw : leadingCoeff D p * leadingCoeff D q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q

Tactic:
rw [← apply_supDegree_add_supDegree hD hadd, ← supDegree_mul hD hadd ?_ hp hq, leadingCoeff]

Premises used: AddMonoidAlgebra.supDegree_mul, AddMonoidAlgebra.leadingCoeff, 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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
ha : leadingCoeff D p ≠ 0
hb : leadingCoeff D q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
apply mul_ne_zero

Premises used: mul_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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
ha : ¬leadingCoeff D p = 0
ha₁ ha₂ ha₃ ha₄ : ¬p = 0
⊢ leadingCoeff D p ≠ 0

Tactic:
rwa [Ne, leadingCoeff_eq_zero hD]

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Ne
-- 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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
hb : ¬leadingCoeff D q = 0
hb₁ hb₂ hb₃ hb₄ : ¬q = 0
⊢ leadingCoeff D q ≠ 0

Tactic:
rwa [Ne, leadingCoeff_eq_zero hD]

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Ne
-- 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
inl : leadingCoeff D (0 * q) = leadingCoeff D 0
inr : ∀ (hp : p ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p
⊢ leadingCoeff D (p * q) = leadingCoeff D p

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
hq : Monic D q
inl inl₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) (leadingCoeff D 0)
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_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
hq : Monic D q
hp : p ≠ 0
inr : (p * q : (a : A) → R) (Function.invFun D (supDegree D (p * q))) = leadingCoeff D p
inr₁ : (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p
inr₂ : leadingCoeff D p * leadingCoeff D q = leadingCoeff D p
inr₃ : leadingCoeff D p * 1 = leadingCoeff D p
inr₄ inr₅ : leadingCoeff D p = leadingCoeff D p
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
rw [leadingCoeff, hq.supDegree_mul_of_ne_zero_left hD hadd hp,
    apply_supDegree_add_supDegree hD hadd, hq, mul_one]

Premises used: AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, AddMonoidAlgebra.leadingCoeff, mul_one, 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
hp : Monic D p
inl : leadingCoeff D (p * 0) = leadingCoeff D 0
inr : ∀ (hq : q ≠ 0), leadingCoeff D (p * q) = leadingCoeff D q
⊢ leadingCoeff D (p * q) = 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 : Monic D p
inl inl₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) (leadingCoeff D 0)
⊢ leadingCoeff D (p * 0) = leadingCoeff D 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_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
inr : (p * q : (a : A) → R) (Function.invFun D (supDegree D (p * q))) = leadingCoeff D q
inr₁ : (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D q
inr₂ : leadingCoeff D p * leadingCoeff D q = leadingCoeff D q
inr₃ : 1 * leadingCoeff D q = leadingCoeff D q
inr₄ inr₅ : leadingCoeff D q = leadingCoeff D q
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Tactic:
rw [leadingCoeff, hp.supDegree_mul_of_ne_zero_right hD hadd hq,
    apply_supDegree_add_supDegree hD hadd, hp, one_mul]

Premises used: AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_right, AddMonoidAlgebra.leadingCoeff, one_mul, 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
hp : Monic D p
hq : Monic D q
rw : leadingCoeff D p = 1
⊢ Monic D (p * q)

Tactic:
rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]

Premises used: AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left, 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
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 : Monic D q
⊢ leadingCoeff D p = 1

Tactic:
hp
-- 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 : Monic D q
⊢ leadingCoeff D p = 1

Tactic:
exact hp
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic.{u_1, u_8, u_9} (R := R) D 1

Tactic:
monic_one hD

Premises used: AddMonoidAlgebra.monic_one
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic.{u_1, u_8, u_9} (R := R) D 1

Tactic:
exact monic_one hD

Premises used: AddMonoidAlgebra.monic_one
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
succ : Monic D (p * p ^ n)
⊢ Monic D (p ^ (n + 1))

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Tactic:
hp.mul hD hadd ih

Premises used: AddMonoidAlgebra.Monic.mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Tactic:
exact hp.mul hD hadd ih

Premises used: AddMonoidAlgebra.Monic.mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
zero : Monic D (HPow.hPow (β := ℕ) p 0)
succ : ∀ (n : ℕ) (ih : Monic D (p ^ n)), Monic D (p ^ (n + 1))
⊢ Monic D (p ^ n)

Tactic:
induction n with
  | zero => rw [pow_zero]; exact monic_one hD
  | succ n ih => rw [pow_succ']; exact hp.mul hD hadd ih

Premises used: pow_zero, AddMonoidAlgebra.monic_one, AddMonoidAlgebra.zero, pow_succ'
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
zero : supDegree.{u_1, u_8, u_9} (R := R) D 1 = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
zero₁ : supDegree.{u_1, u_8, u_9} (R := R) D 1 = 0
zero₂ : supDegree.{u_1, u_8, u_9} (R := R) D (single 0 1) = 0
zero₃ : (if Eq.{u_1 + 1} (α := R) 1 0 then ⊥ else D 0) = 0
zero₄ : D 0 = 0
zero₅ zero₆ : Eq.{u_9 + 1} (α := B) 0 0
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)

Tactic:
rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]

Premises used: AddMonoidAlgebra.supDegree_single, pow_zero, zero_nsmul, one_ne_zero, OfNat.ofNat, if_neg, AddMonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n_1 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
succ : supDegree D (p * p ^ n) = (n + 1) • supDegree D p
succ₁ : supDegree D p + supDegree D (p ^ n) = (n + 1) • supDegree D p
succ₂ : supDegree D p + n • supDegree D p = (n + 1) • supDegree D p
succ₃ succ₄ : supDegree D p + n • supDegree D p = supDegree D p + n • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p

Tactic:
rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']

Premises used: AddMonoidAlgebra.Monic.pow, AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, succ_nsmul', AddMonoidAlgebra.Monic.ne_zero, pow_succ'
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
inst : Semiring R
A : Type u_8
B : Type u_9
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : LinearOrder B
inst_4 : OrderBot B
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst_7 : Nontrivial R
hp : Monic D p
zero : supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
succ : ∀ (n : ℕ) (ih : supDegree D (p ^ n) = n • supDegree D p), supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p
⊢ supDegree D (p ^ n) = n • supDegree D p

Tactic:
induction n with
  | zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
  | succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,
      ih, succ_nsmul']

Premises used: AddMonoidAlgebra.supDegree_single, AddMonoidAlgebra.Monic.pow, pow_zero, zero_nsmul, AddMonoidAlgebra.zero, AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, succ_nsmul', AddMonoidAlgebra.Monic.ne_zero, one_ne_zero, OfNat.ofNat, if_neg, pow_succ', AddMonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : SemilatticeInf T
inst_2 : OrderTop T
D : A → T
f g : R[A]
⊢ infDegree D f ⊓ infDegree D g ≤ infDegree D (f + g)

Tactic:
le_inf_support_add D f g

Premises used: AddMonoidAlgebra.le_inf_support_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : SemilatticeInf T
inst_2 : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
rw : (↑(s.support.inf' hs D) : WithTop T) = (↑(s.support.inf D) : WithTop T)
rw₁ rw₂ : (↑(s.support.inf D) : WithTop T) = (↑(s.support.inf D) : WithTop T)
⊢ s.support.inf (WithTop.some ∘ D) = (↑(s.support.inf D) : WithTop T)

Tactic:
rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

Premises used: Finset.coe_inf', Finset.inf'_eq_inf
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : SemilatticeInf T
inst_2 : OrderTop T
inst_3 : AddZeroClass A
inst_4 : Add T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
D : A →ₙ+ T
f g : R[A]
⊢ HAdd.hAdd (α := T) (infDegree (⇑D : (a : A) → T) f) (infDegree (⇑D : (a : A) → T) g) ≤
    infDegree (⇑D : (a : A) → T) (f * g)

Tactic:
le_inf_support_mul (fun {a b : A} => (map_add D a b).ge) _ _

Premises used: Eq.ge, map_add, AddMonoidAlgebra.le_inf_support_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
g : G
x : k[G]
g' : G
⊢ Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ g : (a : G) → k) g' : k) ((x : (a : G) → k) (g + g') : k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
g : G
x : k[G]
⊢ (x /ᵒᶠ g).support = x.support.preimage (fun (x : G) ↦ g + x) ⋯

Tactic:
rfl

Premises used: Set.Mem, setOf, Finset.map, Set.toFinset, Set.Finite.toFinset, Finset.preimage, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
g : G
⊢ Eq (α := k[G]) (0 /ᵒᶠ g) 0

Tactic:
map_zero (Finsupp.comapDomain.addMonoidHom _)

Premises used: AddMonoidAlgebra.divOf, map_zero, AddMonoidAlgebra, Finsupp.comapDomain.addMonoidHom
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ 0 : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
⊢ x /ᵒᶠ 0 = x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
m : G
⊢ Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ 0 : (a : G) → k) m : k) ((x : (a : G) → k) m : k)

Tactic:
simp only [AddMonoidAlgebra.divOf_apply, zero_add]

Premises used: AddMonoidAlgebra.divOf_apply, zero_add
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x y : k[G]
g : G
⊢ (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g

Tactic:
map_add (Finsupp.comapDomain.addMonoidHom _) _ _

Premises used: AddMonoidAlgebra.divOf, map_add, AddMonoidAlgebra, Finsupp.comapDomain.addMonoidHom
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a b : G
hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ (a + b) : (a : G) → k) m : k) ((x /ᵒᶠ a /ᵒᶠ b : (a : G) → k) m : k)
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a b m : G
⊢ Eq.{u_1 + 1} (α := k) ((x /ᵒᶠ (a + b) : (a : G) → k) m : k) ((x /ᵒᶠ a /ᵒᶠ b : (a : G) → k) m : k)

Tactic:
simp only [AddMonoidAlgebra.divOf_apply, add_assoc]

Premises used: AddMonoidAlgebra.divOf_apply, add_assoc
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((of' k G a * x /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
⊢ of' k G a * x /ᵒᶠ a = x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
m : G
hfg : ∀ m' ∈ x.support, a + m' = a + m ↔ m' = m
⊢ Eq.{u_1 + 1} (α := k) ((of' k G a * x /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)

Tactic:
rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]

Premises used: AddMonoidAlgebra.divOf_apply, AddMonoidAlgebra.of'_apply, AddMonoidAlgebra.single_mul_apply_aux, one_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
m c : G
hc : c ∈ x.support
⊢ a + c = a + m ↔ c = m

Tactic:
add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
a : G
x : k[G]
m c : G
hc : c ∈ x.support
⊢ a + c = a + m ↔ c = m

Tactic:
exact add_right_inj _

Premises used: add_right_inj
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a : G
hfg : ∀ (m : G), Eq.{u_1 + 1} (α := k) ((x * of' k G a /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)
⊢ x * of' k G a /ᵒᶠ a = x

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Division
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : AddCommMonoid G
inst_2 : IsCancelAdd G
x : k[G]
a m : G
hfg : ∀ m' ∈ x.support, m' + a = a + m ↔ m' = m
⊢ Eq.{u_1 + 1} (α := k) ((x * of' k G a /ᵒᶠ a : (a : G) → k) m : k) ((x : (a : G) → k) m : k)

Tactic:
rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]

Premises used: AddMonoidAlgebra.divOf_apply, AddMonoidAlgebra.of'_apply, AddMonoidAlgebra.mul_single_apply_aux, mul_one