R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ (if m < n + 1 then if m = 0 then 1 else 0 else 0) = Polynomial.coeff 1 m
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ Polynomial.coeff (trunc (n + 1) 1) m = Polynomial.coeff 1 m
rw [coeff_trunc, coeff_one]
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : m = 0
⊢ 1 = if 0 = m then 1 else 0

case inl.inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : ¬m = 0
⊢ 0 = if 0 = m then 1 else 0

case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ 0 = if 0 = m then 1 else 0
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
⊢ (if m < n + 1 then if m = 0 then 1 else 0 else 0) = Polynomial.coeff 1 m
split_ifs with H H' <;> rw [Polynomial.coeff_one]
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : 0 < n + 1
⊢ 1 = if 0 = 0 then 1 else 0
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : m = 0
⊢ 1 = if 0 = m then 1 else 0
subst m
no goals
case inl.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : 0 < n + 1
⊢ 1 = if 0 = 0 then 1 else 0
rw [if_pos rfl]
case inl.inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
case inl.inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : ¬m = 0
⊢ 0 = if 0 = m then 1 else 0
symm
no goals
case inl.inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : m < n + 1
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
exact if_neg (Ne.elim (Ne.symm H'))
case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ (if 0 = m then 1 else 0) = 0
case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ 0 = if 0 = m then 1 else 0
symm
case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ ¬0 = m
case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ (if 0 = m then 1 else 0) = 0
refine' if_neg _
case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : ¬0 < n + 1
⊢ False
case inr
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
H : ¬m < n + 1
⊢ ¬0 = m
rintro rfl
case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : ¬0 < n + 1
⊢ 0 < n + 1
case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : ¬0 < n + 1
⊢ False
apply H
no goals
case inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
H : ¬0 < n + 1
⊢ 0 < n + 1
exact Nat.zero_lt_succ _