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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
letI := Classical.decEq ι
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ (homogenization i p).IsHomogeneous p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ (homogenization i p).IsHomogeneous p.totalDegree
Tactic:
rw [homogenization]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ IsHomogeneous (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
⊢ IsHomogeneous (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) p.totalDegree
Tactic:
intro d hd
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : coeff d (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : coeff d (Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
rw [Finsupp.mapDomain, Finsupp.sum, coeff_sum] at hd
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : ∑ x ∈ p.support, coeff d (Finsupp.single (x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)) (p x)) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : ∑ x ∈ p.support, coeff d (Finsupp.single (x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)) (p x)) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
simp_rw [single_eq_monomial, coeff_monomial] at hd
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
contrapose! hd
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Tactic:
have : ∀ (x : ι →₀ ℕ) (_ : x ∈ p.support),
    ¬x + Finsupp.single i (p.totalDegree - x.sum fun (_x : ι) (m : ℕ) => m) = d := by
  intro x hx hh
  apply hd
  rw [← hh, weightedDegree_one]
  change ((x + Finsupp.single i (p.totalDegree - x.sum fun _ m => m)).sum fun _ m => m) = _
  rw [aux hx]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
Tactic:
rw [← Finset.sum_coe_sort]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ i_1 : { x // x ∈ p.support },
      if ↑i_1 + Finsupp.single i (p.totalDegree - (↑i_1).sum fun x m => m) = d then p ↑i_1 else 0) =
    0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ i_1 : { x // x ∈ p.support },
      if ↑i_1 + Finsupp.single i (p.totalDegree - (↑i_1).sum fun x m => m) = d then p ↑i_1 else 0) =
    0
Tactic:
conv_lhs =>
  congr; rfl; ext i
  rw [if_neg (this i.1 i.2)]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ∑ i : { x // x ∈ p.support }, 0 = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ∑ i : { x // x ∈ p.support }, 0 = 0
Tactic:
simp
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
⊢ ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
Tactic:
intro x hx hh
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ False

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ False
Tactic:
apply hd
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (weightedDegree 1) d = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (weightedDegree 1) d = p.totalDegree
Tactic:
rw [← hh, weightedDegree_one]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ degree (x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m)) = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ degree (x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m)) = p.totalDegree
Tactic:
change ((x + Finsupp.single i (p.totalDegree - x.sum fun _ m => m)).sum fun _ m => m) = _
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
x : ι →₀ ℕ
hx : x ∈ p.support
hh : x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
Tactic:
rw [aux hx]
State after:
no goals