σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m (↑(trunc R n) 1) = MvPolynomial.coeff m 1
rw [coeff_trunc, coeff_one]
case inl.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ 0 = MvPolynomial.coeff m 1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1
split_ifs with H H'
case inl.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : 0 < n
⊢ 1 = MvPolynomial.coeff 0 1
case inl.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1
subst m
no goals
case inl.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : 0 < n
⊢ 1 = MvPolynomial.coeff 0 1
simp
case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0
case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1
symm
case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0
rw [MvPolynomial.coeff_one]
no goals
case inl.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
exact if_neg (Ne.symm H')
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ MvPolynomial.coeff m 1 = 0
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ 0 = MvPolynomial.coeff m 1
symm
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ (if 0 = m then 1 else 0) = 0
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ MvPolynomial.coeff m 1 = 0
rw [MvPolynomial.coeff_one]
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ ¬0 = m
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ (if 0 = m then 1 else 0) = 0
refine' if_neg _
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : ¬0 < n
⊢ False
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ ¬0 = m
rintro rfl
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : ¬0 < n
⊢ 0 < n
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : ¬0 < n
⊢ False
apply H
no goals
case inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
H : ¬0 < n
⊢ 0 < n
exact Ne.bot_lt hnn