Getting more info out of a list function

Stream: new members

[Vivek Rajesh Joshi]

I have this function that takes in a list and spits out the index of the first nonzero element with a proof of it being nonzero, along with the remaining tail. Is there a way I can modify this to get the value of that element too, along with perhaps a proof of it being the ith element of the list?

def List.firstNzElt (l : List F) (hl : l.any (·≠0)) : {i : Fin l.length // l.get i ≠ 0}×(List F) :=
  have hl' : l≠[] := by simp at hl; rcases hl with ⟨x,h,_⟩; exact ne_nil_of_mem h
  if hx : l.head hl' ≠ 0
  then (⟨⟨0,length_pos.mpr hl'⟩,by simp [l.get_zero_eq_head hl',hx]⟩,l.tail)
  else
  match l with
  | [] => by contradiction
  | a::as =>
    have has : as.any (·≠0) := by
      simp at hx
      simp [hx] at hl
      simp [hl]
    let (⟨idx,hidx⟩,t) := as.firstNzElt has
    (⟨idx.succ,by simp [hidx]⟩,t)

[Anand Rao Tadipatri]

One way to do this is to push the if...else within the cons case of the match block:

import Mathlib.Tactic

variable {F : Type} [Field F] [DecidableEq F]

def List.firstNzElt (l : List F) (hl : l.any (·≠0)) : (a : Fˣ) × {i : Fin l.length // l.get i = a} ×(List F) :=
  have hl' : l≠[] := by simp at hl; rcases hl with ⟨x,h,_⟩; exact ne_nil_of_mem h
  match l with
  | [] => by contradiction
  | a::as =>
    if ha : a ≠ 0 then
      ⟨⟨a, a⁻¹, CommGroupWithZero.mul_inv_cancel a ha, inv_mul_cancel₀ ha⟩,
      ⟨⟨0, length_pos.mpr hl'⟩, by simp only [length_cons, Fin.zero_eta, get_eq_getElem, Fin.val_zero, getElem_cons_zero]⟩,
      as⟩
    else
      have has : as.any (·≠0) := by
        simp at ha
        simp [ha] at hl
        simp [hl]
      let ⟨v, ⟨idx,hidx⟩, t⟩ := as.firstNzElt has
      ⟨v, ⟨idx.succ, by simp [hidx, @get_cons_succ]⟩,t⟩