σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m (↑(trunc R n) (↑(C σ R) a)) = MvPolynomial.coeff m (↑MvPolynomial.C a)
rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C]
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0
split_ifs with H <;> first |rfl|try simp_all
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ False
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
exfalso
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ m < n
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ False
apply H
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
hnn : ¬n = 0
H : ¬0 < n
⊢ 0 < n
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ m < n
subst m
no goals
case inr.inl.h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
hnn : ¬n = 0
H : ¬0 < n
⊢ 0 < n
exact Ne.bot_lt hnn
no goals
case inr.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : ¬0 = m
⊢ 0 = 0
rfl
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
try simp_all
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
case inr.inl
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a
simp_all