internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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
Tactic:
rwa [totalDegree_leadingTerms]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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
Tactic:
rwa [totalDegree_leadingTerms]
Proof state after:
no goals
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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
Tactic:
rw [this]
Proof state after:
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.totalDegree + q.totalDegree
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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.totalDegree + q.totalDegree
Tactic:
calc
  _ ≤ max (wp * (leadingTerms q)).totalDegree ((leadingTerms p) * wq + wp * wq).totalDegree :=
    totalDegree_add _ _
  _ ≤
      max (wp * (leadingTerms q)).totalDegree
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (le_refl _) (totalDegree_add _ _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (totalDegree_mul _ _) (le_refl _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p).totalDegree + wq.totalDegree)
          (wp.totalDegree + wq.totalDegree)) :=
    (max_le_max (le_refl _) (max_le_max (totalDegree_mul _ _) (totalDegree_mul _ _)))
  _ < p.totalDegree + q.totalDegree := ?_
Proof state after:
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
⊢ max (wp.totalDegree + q.leadingTerms.totalDegree)
      (max (p.leadingTerms.totalDegree + wq.totalDegree) (wp.totalDegree + wq.totalDegree)) <
    p.totalDegree + q.totalDegree
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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
⊢ max (wp.totalDegree + q.leadingTerms.totalDegree)
      (max (p.leadingTerms.totalDegree + wq.totalDegree) (wp.totalDegree + wq.totalDegree)) <
    p.totalDegree + q.totalDegree
Tactic:
simp only [totalDegree_leadingTerms, max_lt_iff, add_lt_add_iff_right, add_lt_add_iff_left]
Proof state after:
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.totalDegree ∧
    wq.totalDegree < q.totalDegree ∧ wp.totalDegree + wq.totalDegree < p.totalDegree + q.totalDegree
Theorem: MvPolynomial.leadingTerms_mul
Proof state before:
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.totalDegree ∧
    wq.totalDegree < q.totalDegree ∧ wp.totalDegree + wq.totalDegree < p.totalDegree + q.totalDegree
Tactic:
exact ⟨tp, tq, add_lt_add tp tq⟩
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_mul_eq
Proof state before:
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).totalDegree = p.totalDegree + q.totalDegree
Tactic:
rw [← totalDegree_leadingTerms, ← totalDegree_leadingTerms p, ← totalDegree_leadingTerms q,
  leadingTerms_mul, IsHomogeneous.totalDegree]
Proof state after:
case hφ
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms.totalDegree + q.leadingTerms.totalDegree)

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

case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply IsHomogeneous.mul <;> simp [isHomogeneous_leadingTerms]
Proof state after:
case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Theorem: MvPolynomial.totalDegree_mul_eq
Proof state before:
case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply mul_ne_zero (leadingTerms_ne_zero hp) (leadingTerms_ne_zero hq)
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_add_of_totalDegree_eq
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ homogenization i (p + q) = homogenization i p + homogenization i q
Tactic:
dsimp [homogenization]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i ((p + q).totalDegree - j.sum fun x m => m)) (p + q) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p +
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m)) q
Theorem: MvPolynomial.homogenization_add_of_totalDegree_eq
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i ((p + q).totalDegree - j.sum fun x m => m)) (p + q) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p +
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m)) q
Tactic:
rw [Finsupp.mapDomain_add, ← h, ← hpq]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_mul
Proof state before:
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
⊢ homogenization i (p * q) = homogenization i p * homogenization i q
Tactic:
by_cases hp : p = 0
Proof state after:
case pos
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : p = 0
⊢ homogenization i (p * q) = homogenization i p * homogenization i q

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

case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ homogenization i (p * q) = homogenization i p * homogenization i q
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ homogenization i (p * q) = homogenization i p * homogenization i q
Tactic:
rw [homogenization, homogenization, homogenization, totalDegree_mul_eq hp hq, ←
  Finsupp.sum_single p, ← Finsupp.sum_single q, Finsupp.mapDomain_sum, Finsupp.mapDomain_sum]
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain
      (fun j =>
        j +
          Finsupp.single i
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              j.sum fun x m => m))
      (Finsupp.sum p Finsupp.single * Finsupp.sum q Finsupp.single) =
    (Finsupp.sum p fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)) *
      Finsupp.sum q fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain
      (fun j =>
        j +
          Finsupp.single i
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              j.sum fun x m => m))
      (Finsupp.sum p Finsupp.single * Finsupp.sum q Finsupp.single) =
    (Finsupp.sum p fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)) *
      Finsupp.sum q fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)
Tactic:
erw [Finset.sum_mul_sum, Finset.sum_mul_sum, ← Finset.sum_product', ← Finset.sum_product']
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain
      (fun j =>
        j +
          Finsupp.single i
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              j.sum fun x m => m))
      (∑ x ∈ p.support ×ˢ q.support, Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.1 (p x.1) *
        (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.2 (q x.2)
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain
      (fun j =>
        j +
          Finsupp.single i
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              j.sum fun x m => m))
      (∑ x ∈ p.support ×ˢ q.support, Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.1 (p x.1) *
        (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.2 (q x.2)
Tactic:
simp only [Finsupp.single_add, Finsupp.sum_single, monomial_mul]
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (∑ x ∈ p.support ×ˢ q.support, Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (∑ x ∈ p.support ×ˢ q.support, Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Tactic:
rw [Finsupp.mapDomain_finset_sum]
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ ∑ i_1 ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
        (Finsupp.single i_1.1 (p i_1.1) * Finsupp.single i_1.2 (q i_1.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ ∑ i_1 ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
        (Finsupp.single i_1.1 (p i_1.1) * Finsupp.single i_1.2 (q i_1.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ ∀ x ∈ p.support ×ˢ q.support,
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
        (Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ ∀ x ∈ p.support ×ˢ q.support,
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
        (Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
Tactic:
intro a ha
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a ∈ p.support ×ˢ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (Finsupp.single a.1 (p a.1) * Finsupp.single a.2 (q a.2)) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.1 (p a.1)) *
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.2 (q a.2))
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a ∈ p.support ×ˢ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (Finsupp.single a.1 (p a.1) * Finsupp.single a.2 (q a.2)) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.1 (p a.1)) *
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.2 (q a.2))
Tactic:
simp only [Finset.mem_product] at ha
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (Finsupp.single a.1 (p a.1) * Finsupp.single a.2 (q a.2)) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.1 (p a.1)) *
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.2 (q a.2))
Theorem: MvPolynomial.homogenization_mul
Proof state before:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (Finsupp.single a.1 (p a.1) * Finsupp.single a.2 (q a.2)) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.1 (p a.1)) *
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
        (Finsupp.single a.2 (q a.2))
Tactic:
rw [Finsupp.mapDomain_single, Finsupp.mapDomain_single]
Proof state after:
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (Finsupp.single a.1 (p a.1) * Finsupp.single a.2 (q a.2)) =
    Finsupp.single (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m)) (p a.1) *
      Finsupp.single (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m)) (q a.2)