R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
⊢ Polynomial.coeff (trunc (n + 1) (↑(C R) a)) m = Polynomial.coeff (↑Polynomial.C a) m
rw [coeff_trunc, coeff_C, Polynomial.coeff_C]
no goals
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
split_ifs with H <;> first |rfl|try simp_all
no goals
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0
rfl
no goals
case inr.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a
try simp_all
no goals
case inr.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a
simp_all