Zulip Chat Archive

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