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
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
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have inr₁ : ∀ (hq : q ≠ 0),
  (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
-- 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 : p ≠ 0
hq : q ≠ 0
⊢ (p * q : (a : A) → R) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have 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
Tactic: obtain ⟨ap, -, hp⟩ := exists_supDegree_mem_support D hp
-- 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_1 : p ≠ 0
hq : q ≠ 0
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
have 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
Tactic: obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq
-- 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_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) (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q
have inr : (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
Tactic: simp_rw [leadingCoeff, hp, hq, ← hadd, Function.leftInverse_invFun 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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have hb : supDegree D p + supDegree D q ∈ Set.range D
Tactic: apply supDegree_eq_of_max
-- 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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
hb : supDegree D p + supDegree D q ∈ Set.range D
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have hmem : Function.invFun D (supDegree D p + supDegree D q) ∈ (p * q).support
Tactic: apply supDegree_eq_of_max
-- 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
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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have hmax : ∀ a ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q
Tactic: apply supDegree_eq_of_max
-- 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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ Set.range D
have hb : supDegree D p + supDegree D q ∈ { toFun := D, map_add' := hadd : A →ₙ+ B }.srange
Tactic: rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
-- 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
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
⊢ supDegree D p + supDegree D q ∈ Set.range D
have hb₁ : ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
Tactic: rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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 ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q
have this : AddLeftMono B
Tactic: have := addLeftMono_of_addLeftStrictMono B
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Degree (hypothesis)
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
⊢ ∀ a ∈ (p * q).support, D a ≤ supDegree D p + supDegree D q
have this₁ : AddRightMono B
Tactic: have := addRightMono_of_addRightStrictMono B
-- 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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
h : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have apply : leadingCoeff D p * leadingCoeff D q ≠ 0
Tactic: apply supDegree_mul hD hadd ?_ hp hq.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
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw : leadingCoeff D p * 1 ≠ 0
Tactic: simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : leadingCoeff D p * 1 ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₁ : leadingCoeff D p ≠ 0
Tactic: simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : leadingCoeff D p * 1 ≠ 0
simp_rw₁ : leadingCoeff D p ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₂ : ¬leadingCoeff D p = 0
Tactic: simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : leadingCoeff D p * 1 ≠ 0
simp_rw₁ : leadingCoeff D p ≠ 0
simp_rw₂ : ¬leadingCoeff D p = 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₃ : ¬p = 0
Tactic: simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]
-- 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
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₄ : ¬False
Tactic: simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]
-- 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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
h : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have apply : leadingCoeff D p * leadingCoeff D q ≠ 0
Tactic: apply supDegree_mul hD hadd ?_ hp.ne_zero hq
-- 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
h : Nontrivial R
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw : 1 * leadingCoeff D q ≠ 0
Tactic: simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : 1 * leadingCoeff D q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₁ : leadingCoeff D q ≠ 0
Tactic: simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : 1 * leadingCoeff D q ≠ 0
simp_rw₁ : leadingCoeff D q ≠ 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₂ : ¬leadingCoeff D q = 0
Tactic: simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]
-- 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
h : Nontrivial R
simp_rw : 1 * leadingCoeff D q ≠ 0
simp_rw₁ : leadingCoeff D q ≠ 0
simp_rw₂ : ¬leadingCoeff D q = 0
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₃ : ¬q = 0
Tactic: simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]
-- 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
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
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
have simp_rw₄ : ¬False
Tactic: simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]
-- 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
hbot : HAdd.hAdd (α := B) ⊥ ⊥ = ⊥
hp : Monic D p
hq : Monic D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inl : Subsingleton R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inr : Nontrivial R → supDegree D (p * q) = supDegree D p + supDegree D q
Tactic: cases subsingleton_or_nontrivial R
-- 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
hbot : HAdd.hAdd (α := B) ⊥ ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inl : supDegree D (0 * q) = supDegree.{u_1, u_3, u_5} (R := R) D 0 + supDegree D q
Tactic: simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
-- 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
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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have 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
Tactic: simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
-- 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
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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have 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
Tactic: simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
-- 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
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
⊢ supDegree D (p * q) = supDegree D p + supDegree D q
have inl₃ : ⊥ = HAdd.hAdd (α := B) ⊥ ⊥
Tactic: simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
-- 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
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
have inl : leadingCoeff D (0 * q) = leadingCoeff D 0 * leadingCoeff D q
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
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
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
have inr : ∀ (hp : p ≠ 0), leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
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
inst_7 : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ leadingCoeff D (0 * q) = leadingCoeff D 0 * leadingCoeff D q
have inl : leadingCoeff D (0 * q) = 0 * leadingCoeff D q
Tactic: simp_rw [leadingCoeff_zero, zero_mul, leadingCoeff_zero]