Theorem: MvPolynomial.homogenization_mul (FltRegular/ReadyForMathlib/Homogenization.lean)

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
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

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
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

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]
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)

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']
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)

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]
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))

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]
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))

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
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))

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
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))

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
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))

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]
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)

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.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)
Tactic:
simp_rw [single_eq_monomial]
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))
      ((monomial a.1) (p a.1) * (monomial a.2) (q a.2)) =
    (monomial (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m))) (p a.1) *
      (monomial (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))) (q a.2)

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))
      ((monomial a.1) (p a.1) * (monomial a.2) (q a.2)) =
    (monomial (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m))) (p a.1) *
      (monomial (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))) (q a.2)
Tactic:
simp only [Finsupp.single_add, monomial_mul]
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))
      ((monomial (a.1 + a.2)) (p a.1 * q a.2)) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.2)

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))
      ((monomial (a.1 + a.2)) (p a.1 * q a.2)) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.2)
Tactic:
erw [Finsupp.mapDomain_single]
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.single (a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - (a.1 + a.2).sum fun x m => m))
      (p a.1 * q a.2) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.2)

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.single (a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - (a.1 + a.2).sum fun x m => m))
      (p a.1 * q a.2) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.2)
Tactic:
congr 1
State after:
case neg.e_a
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
⊢ a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - (a.1 + a.2).sum fun x m => m) =
    a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
      (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))

State before:
case neg.e_a
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
⊢ a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - (a.1 + a.2).sum fun x m => m) =
    a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
      (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))
Tactic:
rw [Finsupp.sum_add_index]
State after:
case neg.e_a
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
⊢ a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - ((a.1.sum fun x m => m) + a.2.sum fun x m => m)) =
    a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
      (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case neg.e_a
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
⊢ a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - ((a.1.sum fun x m => m) + a.2.sum fun x m => m)) =
    a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
      (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
simp only [Finsupp.single_add, Finsupp.single_tsub]
State after:
case neg.e_a
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
⊢ a.1 + a.2 +
      (Finsupp.single i p.totalDegree + Finsupp.single i q.totalDegree -
        (Finsupp.single i (a.1.sum fun x m => m) + Finsupp.single i (a.2.sum fun x m => m))) =
    a.1 + (Finsupp.single i p.totalDegree - Finsupp.single i (a.1.sum fun x m => m)) +
      (a.2 + (Finsupp.single i q.totalDegree - Finsupp.single i (a.2.sum fun x m => m)))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case neg.e_a
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
⊢ a.1 + a.2 +
      (Finsupp.single i p.totalDegree + Finsupp.single i q.totalDegree -
        (Finsupp.single i (a.1.sum fun x m => m) + Finsupp.single i (a.2.sum fun x m => m))) =
    a.1 + (Finsupp.single i p.totalDegree - Finsupp.single i (a.1.sum fun x m => m)) +
      (a.2 + (Finsupp.single i q.totalDegree - Finsupp.single i (a.2.sum fun x m => m)))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
ext j
State after:
case neg.e_a.h
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
j : ι
⊢ (a.1 + a.2 +
        (Finsupp.single i p.totalDegree + Finsupp.single i q.totalDegree -
          (Finsupp.single i (a.1.sum fun x m => m) + Finsupp.single i (a.2.sum fun x m => m))))
      j =
    (a.1 + (Finsupp.single i p.totalDegree - Finsupp.single i (a.1.sum fun x m => m)) +
        (a.2 + (Finsupp.single i q.totalDegree - Finsupp.single i (a.2.sum fun x m => m))))
      j

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case neg.e_a.h
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
j : ι
⊢ (a.1 + a.2 +
        (Finsupp.single i p.totalDegree + Finsupp.single i q.totalDegree -
          (Finsupp.single i (a.1.sum fun x m => m) + Finsupp.single i (a.2.sum fun x m => m))))
      j =
    (a.1 + (Finsupp.single i p.totalDegree - Finsupp.single i (a.1.sum fun x m => m)) +
        (a.2 + (Finsupp.single i q.totalDegree - Finsupp.single i (a.2.sum fun x m => m))))
      j

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
simp only [Pi.add_apply, Finsupp.coe_add, Finsupp.coe_tsub, Pi.sub_apply]
State after:
case neg.e_a.h
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
j : ι
⊢ a.1 j + a.2 j +
      ((Finsupp.single i p.totalDegree) j + (Finsupp.single i q.totalDegree) j -
        ((Finsupp.single i (a.1.sum fun x m => m)) j + (Finsupp.single i (a.2.sum fun x m => m)) j)) =
    a.1 j + ((Finsupp.single i p.totalDegree) j - (Finsupp.single i (a.1.sum fun x m => m)) j) +
      (a.2 j + ((Finsupp.single i q.totalDegree) j - (Finsupp.single i (a.2.sum fun x m => m)) j))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
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
Tactic:
simp [hp]
State after:
no goals

State before:
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
Tactic:
simp [hq]
State after:
no goals

State before:
case neg.e_a.h
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
j : ι
⊢ a.1 j + a.2 j +
      ((Finsupp.single i p.totalDegree) j + (Finsupp.single i q.totalDegree) j -
        ((Finsupp.single i (a.1.sum fun x m => m)) j + (Finsupp.single i (a.2.sum fun x m => m)) j)) =
    a.1 j + ((Finsupp.single i p.totalDegree) j - (Finsupp.single i (a.1.sum fun x m => m)) j) +
      (a.2 j + ((Finsupp.single i q.totalDegree) j - (Finsupp.single i (a.2.sum fun x m => m)) j))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
have : ∀ {f s p q fs ss : ℕ} (_ : fs ≤ p) (_ : ss ≤ q),
    f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss)) := by
  intros f s p q fs ss hP hQ
  zify [add_le_add hP hQ, hP, hQ]
  ring
State after:
case neg.e_a.h
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
⊢ a.1 j + a.2 j +
      ((Finsupp.single i p.totalDegree) j + (Finsupp.single i q.totalDegree) j -
        ((Finsupp.single i (a.1.sum fun x m => m)) j + (Finsupp.single i (a.2.sum fun x m => m)) j)) =
    a.1 j + ((Finsupp.single i p.totalDegree) j - (Finsupp.single i (a.1.sum fun x m => m)) j) +
      (a.2 j + ((Finsupp.single i q.totalDegree) j - (Finsupp.single i (a.2.sum fun x m => m)) j))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case neg.e_a.h
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
⊢ a.1 j + a.2 j +
      ((Finsupp.single i p.totalDegree) j + (Finsupp.single i q.totalDegree) j -
        ((Finsupp.single i (a.1.sum fun x m => m)) j + (Finsupp.single i (a.2.sum fun x m => m)) j)) =
    a.1 j + ((Finsupp.single i p.totalDegree) j - (Finsupp.single i (a.1.sum fun x m => m)) j) +
      (a.2 j + ((Finsupp.single i q.totalDegree) j - (Finsupp.single i (a.2.sum fun x m => m)) j))

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
refine' this _ _ <;> rw [Finsupp.single_apply] <;> split_ifs with h
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) ≤ (Finsupp.single i p.totalDegree) j

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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : ¬i = j
⊢ 0 ≤ (Finsupp.single i p.totalDegree) j

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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) ≤ (Finsupp.single i q.totalDegree) j

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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : ¬i = j
⊢ 0 ≤ (Finsupp.single i q.totalDegree) j

case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0

case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

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
hp : ¬p = 0
hq : ¬q = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
⊢ ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
Tactic:
intros f s p q fs ss hP hQ
State after:
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
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))

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
hp : ¬p✝ = 0
hq : ¬q✝ = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p✝.support ∧ a.2 ∈ q✝.support
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
Tactic:
zify [add_le_add hP hQ, hP, hQ]
State after:
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
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ ↑f + ↑s + (↑p + ↑q - (↑fs + ↑ss)) = ↑f + (↑p - ↑fs) + (↑s + (↑q - ↑ss))

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
hp : ¬p✝ = 0
hq : ¬q✝ = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p✝.support ∧ a.2 ∈ q✝.support
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ ↑f + ↑s + (↑p + ↑q - (↑fs + ↑ss)) = ↑f + (↑p - ↑fs) + (↑s + (↑q - ↑ss))
Tactic:
ring
State after:
no goals

State before:
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) ≤ (Finsupp.single i p.totalDegree) j
Tactic:
simp only [h, Finsupp.single_eq_same]
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) ≤ p.totalDegree

State before:
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) ≤ p.totalDegree
Tactic:
convert Finset.le_sup (α := ℕ) ha.left
State after:
case h.e'_3
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) = a.1.sum fun x e => e

State before:
case h.e'_3
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.1.sum fun x m => m) = a.1.sum fun x e => e
Tactic:
rfl
State after:
no goals

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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : ¬i = j
⊢ 0 ≤ (Finsupp.single i p.totalDegree) j
Tactic:
simp
State after:
no goals

State before:
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) ≤ (Finsupp.single i q.totalDegree) j
Tactic:
simp only [h, Finsupp.single_eq_same]
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) ≤ q.totalDegree

State before:
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) ≤ q.totalDegree
Tactic:
convert Finset.le_sup (α := ℕ) ha.right
State after:
case h.e'_3
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) = a.2.sum fun x e => e

State before:
case h.e'_3
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) = a.2.sum fun x e => e
Tactic:
rfl
State after:
no goals

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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : ¬i = j
⊢ 0 ≤ (Finsupp.single i q.totalDegree) j
Tactic:
simp
State after:
no goals

State before:
case neg.e_a.h_zero
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, 0 = 0
Tactic:
intro i _
State after:
case neg.e_a.h_zero
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
i : ι
a✝ : i ∈ a.1.support ∪ a.2.support
⊢ 0 = 0

State before:
case neg.e_a.h_zero
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
i : ι
a✝ : i ∈ a.1.support ∪ a.2.support
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
intro i
State after:
case neg.e_a.h_add
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
i : ι
⊢ i ∈ a.1.support ∪ a.2.support → ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case neg.e_a.h_add
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
i : ι
⊢ i ∈ a.1.support ∪ a.2.support → ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
simp
State after:
no goals