Get hypotheses for pattern-matching `let`

Stream: new members

[Vivek Rajesh Joshi]

def List.firstNzElt (l : List F) (hl : l.any (·≠0)) : (x : Fˣ)×{i : Fin l.length // l.get i = x}×(List F) :=
  match l with
  | [] => by contradiction
  | a::as =>
    if ha : a = 0 then
    have has : as.any (·≠0) := anyNz_headZero_tailAnyNz as (ha ▸ hl)
    let ⟨⟨x,xinv,hinv1,hinv2⟩,⟨idx,hidx⟩,t⟩ := as.firstNzElt has
    ⟨⟨x,xinv,hinv1,hinv2⟩,⟨idx.succ,hidx⟩,t⟩
    else
    ⟨⟨a,a⁻¹,CommGroupWithZero.mul_inv_cancel a ha,inv_mul_cancel ha⟩,⟨⟨0,Nat.zero_lt_succ as.length⟩,rfl⟩,as⟩

--example proof
example (l : List F) (hl : l.any (·≠0)) : (l.firstNzElt hl).2.2.length ≥ 0 := by
  let ⟨⟨x,_,_,_⟩,⟨idx,_⟩,t⟩ := (l.firstNzElt hl)
  sorry

In the above proof, how do I introduce hypotheses into the context that state (l.firstNzElt hl).1 = x, (l.firstNzElt hl).2.1 = idx, and so on? Can it be done without having to set all of them individually?

[Eric Wieser]

If you use match rhs with instead of let _ := rhs, you can then write match h : rhs with

[Vivek Rajesh Joshi]

How do I split h into different hypotheses for each term?

[Daniel Weber]

simp should probably work for that

[Vivek Rajesh Joshi]

Nope, simp at h leads to no changes

[Daniel Weber]

Could you send a #mwe?

[Vivek Rajesh Joshi]

I think the above mwe should suffice, but here's the actual case where I want to use it:

import Mathlib.Data.Matrix.Notation

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

structure ReducedRowNz (F : Type) [Field F] [DecidableEq F] where
  z : Nat
  tail : List F

def List.firstNzElt (l : List F) (hl : l.any (·≠0)) : (x : Fˣ)×{i : Fin l.length // l.get i = x}×(List F) :=
  match l with
  | [] => by contradiction
  | a::as =>
    if ha : a = 0 then
    have has : as.any (·≠0) := by sorry
    let ⟨⟨x,xinv,hinv1,hinv2⟩,⟨idx,hidx⟩,t⟩ := as.firstNzElt has
    ⟨⟨x,xinv,hinv1,hinv2⟩,⟨idx.succ,hidx⟩,t⟩
    else
    ⟨⟨a,a⁻¹,CommGroupWithZero.mul_inv_cancel a ha,inv_mul_cancel ha⟩,⟨⟨0,Nat.zero_lt_succ as.length⟩,rfl⟩,as⟩

def ReducedRowNz.toList (row : ReducedRowNz F) : List F := (List.replicate row.z 0).append (1::row.tail)

def List.isReducedRowNz (l : List F) := ∃ r : ReducedRowNz F, r.toList = l

theorem List.firstNzElt_1_isReducedRowNz (l : List F) (hl : l.any (·≠0)) : (l.firstNzElt hl).1 = 1 → l.isReducedRowNz := by
  intro he
  -- match h : (l.firstNzElt hl) with
  -- | ⟨⟨x,_,_,_⟩,⟨idx,_⟩,t⟩ =>
  -- simp at h
  set x := (l.firstNzElt hl).1 with hx
  set idx := (l.firstNzElt hl).2.1 with hidx
  set t := (l.firstNzElt hl).2.2 with ht
  let r : ReducedRowNz F := ⟨idx,t⟩
  use r
  dsimp [ReducedRowNz.toList]
  sorry