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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
⊢ p = C (coeff 0 p)
Tactic:
letI := Classical.decEq ι
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree = 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
Tactic:
erw [Finset.sup_eq_bot_iff] at hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ∀ s ∈ p.support, (s.sum fun x e => e) = ⊥
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : ∀ s ∈ p.support, (s.sum fun x e => e) = ⊥
this : DecidableEq ι := Classical.decEq ι
⊢ p = C (coeff 0 p)
Tactic:
simp only [mem_support_iff] at hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
⊢ p = C (coeff 0 p)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
⊢ p = C (coeff 0 p)
Tactic:
ext m
State after:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

State before:
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
by_cases hm : m = 0
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
rw [coeff_C, if_neg (Ne.symm hm)]
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
Tactic:
classical
by_contra h
specialize hp m h
apply hm
rw [Finsupp.sum] at hp
simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp
ext
simp [hp]
State after:
no goals

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : m = 0
⊢ coeff m p = coeff m (C (coeff 0 p))
Tactic:
simp [hm]
State after:
no goals

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
⊢ coeff m p = 0
Tactic:
by_contra h
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
⊢ False

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
hp : ∀ (s : ι →₀ ℕ), coeff s p ≠ 0 → (s.sum fun x e => e) = ⊥
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
⊢ False
Tactic:
specialize hp m h
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ False

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ False
Tactic:
apply hm
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ m = 0

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : (m.sum fun x e => e) = ⊥
⊢ m = 0
Tactic:
rw [Finsupp.sum] at hp
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∑ a ∈ m.support, m a = ⊥
⊢ m = 0

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∑ a ∈ m.support, m a = ⊥
⊢ m = 0
Tactic:
simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
⊢ m = 0

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
⊢ m = 0
Tactic:
ext
State after:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
a✝ : ι
⊢ m a✝ = 0 a✝

State before:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
m : ι →₀ ℕ
hm : ¬m = 0
h : ¬coeff m p = 0
hp : ∀ (x : ι), m x = 0
a✝ : ι
⊢ m a✝ = 0 a✝
Tactic:
simp [hp]
State after:
no goals