cases on fin 1

Stream: Is there code for X?

[Vasily Ilin]

How do I prove example (i : fin 1) : i = 0 ∨ i = 1? cases i does not work.

[Vasily Ilin]

I need it for this proof:

import tactic -- imports all the Lean tactics
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module
import data.matrix.notation

open complex

example : linear_independent ℝ ![1+I, 1-I] :=
begin
  rw fintype.linear_independent_iff,
  intros g h i,
  simp [fin.sum_univ_succ, ext_iff] at h,
  have h1: g 0 + g 1 + (g 0 + - g 1) = 0+0,
    exact congr (congr_arg has_add.add h.left) h.right,
  have h2: g 0 + g 1 - (g 0 + - g 1) = 0-0,
    exact congr (congr_arg has_sub.sub h.left) h.right,
  ring_nf at h1,
  ring_nf at h2,
  suggest,
  -- wanna do cases i
  sorry,
end

[Kyle Miller]

tactic#fin_cases should work here, as fin_cases i

[Heather Macbeth]

By the way, do you know about the linear_combination tactic? It will give the values of g 0 and g 1 much more easily.

have h1 : g 0 = 0 := by linear_combination (h.1, 1/2) (h.2, 1/2),