internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.homogenization_mul
Proof 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
Proof 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
Theorem: MvPolynomial.homogenization_mul
Proof 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
Proof state after:
no goals
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
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
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_mul
Proof 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 _
Proof 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
Theorem: MvPolynomial.homogenization_mul
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_mul
Proof 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
Proof 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₂
Theorem: MvPolynomial.homogenization_mul
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
⊢ homogenization i (X j + C r) = X j + C r * X i
Tactic:
nontriviality R
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ homogenization i (X j + C r) = X j + C r * X i
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ homogenization i (X j + C r) = X j + C r * X i
Tactic:
erw [homogenization, Finsupp.mapDomain_add, Finsupp.mapDomain_single, Finsupp.mapDomain_single]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single
        (Finsupp.single j 1 + Finsupp.single i ((X j + C r).totalDegree - (Finsupp.single j 1).sum fun x m => m)) 1 +
      Finsupp.single (0 + Finsupp.single i ((X j + C r).totalDegree - Finsupp.sum 0 fun x m => m)) r =
    X j + C r * X i
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single
        (Finsupp.single j 1 + Finsupp.single i ((X j + C r).totalDegree - (Finsupp.single j 1).sum fun x m => m)) 1 +
      Finsupp.single (0 + Finsupp.single i ((X j + C r).totalDegree - Finsupp.sum 0 fun x m => m)) r =
    X j + C r * X i
Tactic:
simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, this, add_zero,
  Finsupp.single_zero, zero_add, single_eq_monomial]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + (monomial (Finsupp.single i 1)) r = X j + C r * X i
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + (monomial (Finsupp.single i 1)) r = X j + C r * X i
Tactic:
rw [X, X, ← C_mul_X_pow_eq_monomial, pow_one]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + C r * X i =
    (monomial (Finsupp.single j 1)) 1 + C r * (monomial (Finsupp.single i 1)) 1
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + C r * X i =
    (monomial (Finsupp.single j 1)) 1 + C r * (monomial (Finsupp.single i 1)) 1
Tactic:
congr
Proof state after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single j 1 + Finsupp.single i (1 - 1) = Finsupp.single j 1
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single j 1 + Finsupp.single i (1 - 1) = Finsupp.single j 1
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j + C r).totalDegree = 1
Tactic:
rw [totalDegree_add_eq_left_of_totalDegree_lt]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j).totalDegree = 1

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j).totalDegree
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j).totalDegree = 1
Tactic:
exact totalDegree_X _
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j).totalDegree
Tactic:
simp only [totalDegree_C, totalDegree_X, Nat.lt_one_iff]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_sub_C
Proof state before:
R✝ : Type ?u.241614
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
r : R
⊢ homogenization i (X j - C r) = X j - C r * X i
Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← C_neg, homogenization_X_add_C, C_neg, neg_mul]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
Tactic:
nontriviality R
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
Tactic:
erw [homogenization, Finsupp.mapDomain_add]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (X j ^ n) +
      Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (C r) =
    X j ^ n + C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (X j ^ n) +
      Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (C r) =
    X j ^ n + C r * X i ^ n
Tactic:
erw [AddMonoidAlgebra.single_pow]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n)) +
      Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (C r) =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n)) +
      Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (C r) =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Tactic:
erw [Finsupp.mapDomain_single, Finsupp.mapDomain_single]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single
        (n • Finsupp.single j 1 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree -
              (n • Finsupp.single j 1).sum fun x m => m))
        (1 ^ n) +
      Finsupp.single
        (0 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - Finsupp.sum 0 fun x m => m))
        r =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single
        (n • Finsupp.single j 1 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree -
              (n • Finsupp.single j 1).sum fun x m => m))
        (1 ^ n) +
      Finsupp.single
        (0 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - Finsupp.sum 0 fun x m => m))
        r =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Tactic:
simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, zero_add,
  single_eq_monomial, one_pow, mul_one, Finsupp.smul_single', Finsupp.single_tsub]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial
          (Finsupp.single j n +
            (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n)))
        1 +
      (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r =
    (monomial (Finsupp.single j n)) 1 + C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial
          (Finsupp.single j n +
            (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n)))
        1 +
      (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r =
    (monomial (Finsupp.single j n)) 1 + C r * X i ^ n
Tactic:
congr
Proof state after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r = C r * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n + C r).totalDegree = n
Tactic:
rw [totalDegree_add_eq_left_of_totalDegree_lt]
Proof state after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n).totalDegree = n

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j ^ n).totalDegree
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n).totalDegree = n
Tactic:
exact totalDegree_X_pow _ _
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j ^ n).totalDegree
Tactic:
simp only [totalDegree_C, totalDegree_X_pow, hn]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n) =
    Finsupp.single j n
Tactic:
rw [totalDegree_add_eq_left_of_totalDegree_lt]
Proof state after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Tactic:
simp [one_ne_zero]
Proof state after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Tactic:
simp [one_ne_zero, hn]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case e_a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r = C r * X i ^ n
Tactic:
convert (C_mul_X_pow_eq_monomial (R := R)).symm
Proof state after:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = ((monomial (Finsupp.single j n)) 1 + C r).totalDegree
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = ((monomial (Finsupp.single j n)) 1 + C r).totalDegree
Tactic:
rw [← C_mul_X_pow_eq_monomial]
Proof state after:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = (C 1 * X j ^ n + C r).totalDegree
Theorem: MvPolynomial.homogenization_X_pow_add_C
Proof state before:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = (C 1 * X j ^ n + C r).totalDegree
Tactic:
simp [this]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_sub_C
Proof state before:
R✝ : Type ?u.276957
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
r : R
⊢ homogenization i (X j ^ n - C r) = X j ^ n - C r * X i ^ n
Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← C_neg, homogenization_X_pow_add_C hn, C_neg, neg_mul]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_sub_one
Proof state before:
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ homogenization i (X j ^ n - 1) = X j ^ n - X i ^ n
Tactic:
convert homogenization_X_pow_sub_C hn (R := R) _
Proof state after:
case h.e'_3.h.e'_6
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_sub_one
Proof state before:
case h.e'_3.h.e'_6
R✝ : Type ?u.286962
ι : Type u_2
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : CommRing R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_X_pow_add_one
Proof state before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
⊢ homogenization i (X j ^ n + 1) = X j ^ n + X i ^ n
Tactic:
convert homogenization_X_pow_add_C (R := R) hn _
Proof state after:
case h.e'_3.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n
Theorem: MvPolynomial.homogenization_X_pow_add_one
Proof state before:
case h.e'_3.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
⊢ X i ^ n = C 1 * X i ^ n
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof state before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
Tactic:
letI := Classical.decEq α
Proof state after:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof state before:
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
S : Finset α
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
Tactic:
induction' S using Finset.induction with s S hs hsi
Proof state after:
case empty
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ ∅, (monomial (g v)) (f v)).support ⊆ image g ∅

case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ v ∈ insert s S, (monomial (g v)) (f v)).support ⊆ image g (insert s S)
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof state before:
case empty
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
⊢ (∑ v ∈ ∅, (monomial (g v)) (f v)).support ⊆ image g ∅
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.support_sum_monomial_subset'
Proof state before:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ (∑ v ∈ insert s S, (monomial (g v)) (f v)).support ⊆ image g (insert s S)
Tactic:
rw [Finset.sum_insert hs]
Proof state after:
case insert
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s) + ∑ x ∈ S, (monomial (g x)) (f x)).support ⊆ image g (insert s S)