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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
classical
rw [Finsupp.sum_add_index]
rw [Finsupp.sum_single_index]
rw [add_tsub_cancel_iff_le]
apply Finset.le_sup hp
rfl
intros
rfl
intros
rfl
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
rw [Finsupp.sum_add_index]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x.sum fun x m => m) + (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x.sum fun x m => m) + (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rw [Finsupp.sum_single_index]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) + (p.totalDegree - x.sum fun x m => m) = p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) + (p.totalDegree - x.sum fun x m => m) = p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rw [add_tsub_cancel_iff_le]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) ≤ p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ (x.sum fun x m => m) ≤ p.totalDegree

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
apply Finset.le_sup hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ 0 = 0

case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rfl
State after:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
intros
State after:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
⊢ 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case h_zero
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
⊢ 0 = 0

case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
rfl
State after:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂

State before:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ∀ a ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
Tactic:
intros
State after:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
b₁✝ b₂✝ : ℕ
⊢ b₁✝ + b₂✝ = b₁✝ + b₂✝

State before:
case h_add
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
a✝¹ : ι
a✝ : a✝¹ ∈ x.support ∪ (Finsupp.single i (p.totalDegree - x.sum fun x m => m)).support
b₁✝ b₂✝ : ℕ
⊢ b₁✝ + b₂✝ = b₁✝ + b₂✝
Tactic:
rfl
State after:
no goals