## Stream: new members

### Topic: Failed to synthesize instance for zero index of list

#### Ioannis Konstantoulas (Sep 11 2023 at 10:23):

In the middle of a proof, I have a list L together with an equation : L = x :: y :: ys. Using that, I prove

have positive_length : 0 < L.length := sorry


I then write something like

let l_0 := (0 : Fin L.length)


and get the error message

failed to synthesize instance
OfNat (Fin (List.length L)) 0


How can I use positive_length to make Lean synthesize that instance for me, so I can use it in the proof?

#### Yaël Dillies (Sep 11 2023 at 10:25):

You must wrap it in a Fact.

#### Ioannis Konstantoulas (Sep 11 2023 at 10:26):

The conclusion of my theorem is of the form ∃ i : Fin L.length, p L[i] for a predicate p.

#### Ioannis Konstantoulas (Sep 11 2023 at 10:26):

Yaël Dillies said:

You must wrap it in a Fact.

Is Fact a type in Core? I am not using Mathlib or Std.

#### Yaël Dillies (Sep 11 2023 at 10:27):

docs#Fin.instAddMonoidWithOne tells you what you need. You need docs#NeZero.

#### Yaël Dillies (Sep 11 2023 at 10:28):

Tough luck. Core and Std only have a OfNat (Fin n.succ) instance, not a Fact (n != 0) -> OfNat (Fin n) as mathlib does.

#### Ioannis Konstantoulas (Sep 11 2023 at 10:32):

I am confused by that statement: previously in the proof, I wrote (0 : Fin 1) with no complaints. Do you mean that I should prove L.length = succ x for some x? That is easy.

#### Yaël Dillies (Sep 11 2023 at 10:34):

Yeah because 1 is syntactically of the form Nat.succ n for some n (namely n := 0). The problem in your case is that L.length is not syntactically of the form Nat.succ n for some n.

#### Eric Wieser (Sep 11 2023 at 11:19):

(1 is not syntactically succ n, but it does unify with it)