## Stream: new members

### Topic: Solving ite goals

#### Hanting Zhang (Jan 07 2021 at 23:19):

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 (Jan 07 2021 at 23:20):

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

#### Kevin Buzzard (Jan 07 2021 at 23:41):

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

#### Adam Topaz (Jan 07 2021 at 23:42):

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]


Last updated: Dec 20 2023 at 11:08 UTC