internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ∀ s ∈ p.support, (s.sum fun x e => e) = ⊥
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
Tactic:
simp only [mem_support_iff] at hp
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
⊢ p = C (coeff 0 p)
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
⊢ p = C (coeff 0 p)
Tactic:
ext m
Proof state after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
by_cases hm : m = 0
Proof state after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
rw [coeff_C, if_neg (Ne.symm hm)]
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
Tactic:
classical
by_contra h
specialize hp m h
apply hm
rw [Finsupp.sum] at hp
simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp
ext
simp [hp]
Proof state after:
no goals
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
simp [hm]
Proof state after:
no goals
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
Tactic:
by_contra h
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
⊢ False
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
⊢ False
Tactic:
specialize hp m h
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ False
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ False
Tactic:
apply hm
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ m = 0
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ m = 0
Tactic:
rw [Finsupp.sum] at hp
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∑ a ∈ m.support, m a = ⊥
⊢ m = 0
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∑ a ∈ m.support, m a = ⊥
⊢ m = 0
Tactic:
simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp
Proof state after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
⊢ m = 0
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
⊢ m = 0
Tactic:
ext
Proof state after:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
a✝ : ι
⊢ m a✝ = 0 a✝
Theorem: MvPolynomial.eq_C_of_totalDegree_zero
Proof state before:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
a✝ : ι
⊢ m a✝ = 0 a✝
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
by_cases hp : p.totalDegree = 0
Proof state after:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
by_cases hq : q.totalDegree = 0
Proof state after:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rcases eq_leadingTerms_add p hp with ⟨wp, hp, tp⟩
Proof state after:
case neg.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rcases eq_leadingTerms_add q hq with ⟨wq, hq, tq⟩
Proof state after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [hp, hq]
Proof state after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ ((p.leadingTerms + wp) * (q.leadingTerms + wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ ((p.leadingTerms + wp) * (q.leadingTerms + wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Tactic:
simp only [add_mul, mul_add]
Proof state after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms + wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms + wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Tactic:
rw [add_assoc, leadingTerms_add_of_totalDegree_lt, leadingTerms_add_of_totalDegree_lt,
  leadingTerms_add_of_totalDegree_lt, leadingTerms_idempotent, leadingTerms_idempotent,
  leadingTerms_eq_self_iff_isHomogeneous]
Proof state after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms * q.leadingTerms).totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wq.totalDegree < q.leadingTerms.totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wp.totalDegree < p.leadingTerms.totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < (p.leadingTerms * q.leadingTerms).totalDegree
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [eq_C_of_totalDegree_zero hp, leadingTerms_C_mul, leadingTerms_C]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [eq_C_of_totalDegree_zero hq, mul_comm, leadingTerms_C_mul, leadingTerms_C, mul_comm]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
Tactic:
rw [IsHomogeneous.totalDegree]
Proof state after:
case hφ
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case hφ
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply IsHomogeneous.mul (isHomogeneous_leadingTerms p) (isHomogeneous_leadingTerms q)
Proof state after:
case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply mul_ne_zero
Proof state after:
case h.ha
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms ≠ 0

case h.hb
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q.leadingTerms ≠ 0
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.ha
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms ≠ 0
Tactic:
apply leadingTerms_ne_zero
Proof state after:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p ≠ 0
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p ≠ 0
Tactic:
rintro rfl
Proof state after:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
q : MvPolynomial ι S
hq : ¬q.totalDegree = 0
hp : ¬totalDegree 0 = 0
⊢ False
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
q : MvPolynomial ι S
hq : ¬q.totalDegree = 0
hp : ¬totalDegree 0 = 0
⊢ False
Tactic:
exact hp totalDegree_zero
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.hb
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q.leadingTerms ≠ 0
Tactic:
apply leadingTerms_ne_zero
Proof state after:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q ≠ 0
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q ≠ 0
Tactic:
rintro rfl
Proof state after:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬totalDegree 0 = 0
⊢ False
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬totalDegree 0 = 0
⊢ False
Tactic:
exact hq totalDegree_zero
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms * q.leadingTerms).totalDegree
Tactic:
rw [this]
Proof state after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)
Tactic:
exact IsHomogeneous.mul (isHomogeneous_leadingTerms p) (isHomogeneous_leadingTerms q)
Proof state after:
no goals