awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0 * leadingCoeff D q
have inl₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 0
Tactic: simp_rw [leadingCoeff_zero, zero_mul, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
have inr : leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
have inr₁ : ∀ (hq : q ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
Tactic: obtain rfl | hq := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0
have inr : leadingCoeff D (p * 0) = leadingCoeff D p * 0
Tactic: simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0
have inr₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) 0
Tactic: simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
have rw : leadingCoeff D p * leadingCoeff D q ≠ 0
Tactic: rw [← apply_supDegree_add_supDegree hD hadd, ← supDegree_mul hD hadd ?_ hp hq, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have ha : leadingCoeff D p ≠ 0
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have hb : leadingCoeff D q ≠ 0
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D p ≠ 0
have ha : ¬leadingCoeff D p = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D p ≠ 0
have ha₁ : ¬p = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D q ≠ 0
have hb : ¬leadingCoeff D q = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D q ≠ 0
have hb₁ : ¬q = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero hD]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inl : leadingCoeff D (0 * q) = leadingCoeff D 0
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr : ∀ (hp : p ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0
have inl : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) (leadingCoeff D 0)
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr : (p * q : (a : A) → R) (Function.invFun D (supDegree 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr₁ : (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr₂ : leadingCoeff D p * leadingCoeff D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr₃ : leadingCoeff D p * 1 = 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p
have inr₄ : leadingCoeff D p = 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inl : leadingCoeff D (p * 0) = leadingCoeff D 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr : ∀ (hq : q ≠ 0), leadingCoeff D (p * q) = leadingCoeff D q
Tactic: obtain rfl | hq := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * 0) = leadingCoeff D 0
have inl : Eq.{u_1 + 1} (α := R) (leadingCoeff D 0) (leadingCoeff D 0)
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr : (p * q : (a : A) → R) (Function.invFun D (supDegree 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr₁ : (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr₂ : leadingCoeff D p * leadingCoeff D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr₃ : 1 * leadingCoeff D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ leadingCoeff D (p * q) = leadingCoeff D q
have inr₄ : leadingCoeff D 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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ Monic D (p * q)
have rw : leadingCoeff D p = 1
Tactic: rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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 ^ (n + 1))
have succ : Monic D (p * p ^ n)
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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 D (p ^ n)
have zero : Monic D (HPow.hPow (β := ℕ) p 0)
Tactic: induction n with
  | zero => rw [pow_zero]; exact monic_one hD
  | succ n ih => rw [pow_succ']; exact hp.mul hD hadd ih
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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)
⊢ Monic D (p ^ n)
have succ : ∀ (n : ℕ) (ih : Monic D (p ^ n)), Monic D (p ^ (n + 1))
Tactic: induction n with
  | zero => rw [pow_zero]; exact monic_one hD
  | succ n ih => rw [pow_succ']; exact hp.mul hD hadd ih
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
have zero : supDegree.{u_1, u_8, u_9} (R := R) D 1 = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
Tactic: rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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)
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
have zero₁ : supDegree.{u_1, u_8, u_9} (R := R) D 1 = 0
Tactic: rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
have zero₂ : supDegree.{u_1, u_8, u_9} (R := R) D (single 0 1) = 0
Tactic: rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (goal)
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
⊢ supDegree D (HPow.hPow (β := ℕ) p 0) = HSMul.hSMul (α := ℕ) 0 (supDegree D p)
have zero₃ : (if Eq.{u_1 + 1} (α := R) 1 0 then ⊥ else D 0) = 0
Tactic: rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]