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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
⊢ p.leadingTerms = p ↔ p.IsHomogeneous p.totalDegree
Tactic:
constructor <;> intro h
State after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ p.IsHomogeneous p.totalDegree

case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ p.leadingTerms = p

State before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ p.IsHomogeneous p.totalDegree
Tactic:
rw [IsHomogeneous, IsWeightedHomogeneous]
State after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ ∀ ⦃d : ι →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree 1) d = p.totalDegree

State before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.leadingTerms = p
⊢ ∀ ⦃d : ι →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree 1) d = p.totalDegree
Tactic:
contrapose! h
State after:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : ∃ d, coeff d p ≠ 0 ∧ (weightedDegree 1) d ≠ p.totalDegree
⊢ p.leadingTerms ≠ p

State before:
case mp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : ∃ d, coeff d p ≠ 0 ∧ (weightedDegree 1) d ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Tactic:
rcases h with ⟨h_w, h_h₁, h_h₂⟩
State after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ p.leadingTerms ≠ p

State before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ p.leadingTerms ≠ p
Tactic:
rw [leadingTerms, Ne, MvPolynomial.ext_iff]
State after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ¬∀ (m : ι →₀ ℕ), coeff m ((homogeneousComponent p.totalDegree) p) = coeff m p

State before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ¬∀ (m : ι →₀ ℕ), coeff m ((homogeneousComponent p.totalDegree) p) = coeff m p
Tactic:
push_neg
State after:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ∃ m, coeff m ((homogeneousComponent p.totalDegree) p) ≠ coeff m p

State before:
case mp.intro.intro
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ ∃ m, coeff m ((homogeneousComponent p.totalDegree) p) ≠ coeff m p
Tactic:
use h_w
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
classical
rw [weightedDegree_one] at h_h₂
change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂
simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
  not_false_iff, not_forall, ite_eq_left_iff]
convert h_h₂
State after:
no goals

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : (weightedDegree 1) h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
rw [weightedDegree_one] at h_h₂
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : degree h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : degree h_w ≠ p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ coeff h_w ((homogeneousComponent p.totalDegree) p) ≠ coeff h_w p
Tactic:
simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne,
  not_false_iff, not_forall, ite_eq_left_iff]
State after:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ ¬degree h_w = p.totalDegree

State before:
case h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h_w : ι →₀ ℕ
h_h₁ : coeff h_w p ≠ 0
h_h₂ : ¬(h_w.sum fun _x e => e) = p.totalDegree
⊢ ¬degree h_w = p.totalDegree
Tactic:
convert h_h₂
State after:
no goals

State before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ p.leadingTerms = p
Tactic:
rw [leadingTerms_apply]
State after:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) = p

State before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) = p
Tactic:
rw [(_ :
    (p.support.filter fun s : ι →₀ ℕ => ∑ i : ι in s.support, s i = p.totalDegree) =
      p.support)]
State after:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support

State before:
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p
Tactic:
rw [support_sum_monomial_coeff p]
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support
Tactic:
rw [Finset.filter_eq_self]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∀ x ∈ p.support, ∑ i ∈ x.support, x i = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∀ x ∈ p.support, ∑ i ∈ x.support, x i = p.totalDegree
Tactic:
intro s hs
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∑ i ∈ s.support, s i = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : s ∈ p.support
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Tactic:
rw [mem_support_iff] at hs
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = p.totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = p.totalDegree
Tactic:
rw [← h hs, weightedDegree_one]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = degree s

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
s : ι →₀ ℕ
hs : coeff s p ≠ 0
⊢ ∑ i ∈ s.support, s i = degree s
Tactic:
rfl
State after:
no goals