Solving ite goals

Stream: new members

[Hanting Zhang]

I'm trying to golf this proof, but I'm not sure how to apply n ≠ 0 to the if-else goal after the first rewrite.

import tactic
import ring_theory.polynomial.basic
import algebra.polynomial.big_operators

universes u v
open_locale big_operators
open polynomial fin finset

-- in polynomial.
theorem coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) : (C a).coeff n = 0 :=
begin
  rw polynomial.coeff_C,
  simp,
  intro hn,
  exfalso,
  apply h,
  exact hn,
end

[Hanting Zhang]

Is there a one-line way to do this? (Also, yes, I have a non-terminal simp.)

[Kevin Buzzard]

What's the goal after the rewrite? If it's an ite you can use if_neg

[Adam Topaz]

Here's a 2-line proof: a one line proof

theorem coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) : (C a).coeff n = 0 :=
by finish [coeff_C]