-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_cons_cons_fst_get_zero
    (x : α) (xs y ys) (w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length) :
    (suffixLevenshtein C (x :: xs) (y :: ys)).1[0]'w =
      let ⟨dx, _⟩ := suffixLevenshtein C xs (y :: ys)
      let ⟨dy, _⟩ := suffixLevenshtein C (x :: xs) ys
      let ⟨dxy, _⟩ := suffixLevenshtein C xs ys
      min
        (C.delete x + dx[0])
        (min
          (C.insert y + dy[0])
          (C.substitute x y + dxy[0]))

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (impl C (x :: xs) y (suffixLevenshtein C (x :: xs) ys)).val[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | ⟨dx, property⟩ =>
      match suffixLevenshtein C (x :: xs) ys with
      | ⟨dy, property_1⟩ =>
        match suffixLevenshtein C xs ys with
        | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))

Tactic:
simp only [suffixLevenshtein_cons₁]

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (impl C (x :: xs) y ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩).val[0] =
    min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0])
      (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0])
        (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (match impl C xs y ⟨(suffixLevenshtein C xs ys).val, ?w'⟩ with
    | ⟨r, w⟩ =>
      min (C.delete x + r[0])
        (min (C.insert y + levenshtein C (x :: xs) ys) (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))) =
    min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0])
      (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0])
        (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))

case w'
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ 0 < (suffixLevenshtein C xs ys).val.length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (suffixLevenshtein C (x :: xs) (y :: ys)).val[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | ⟨dx, property⟩ =>
      match suffixLevenshtein C (x :: xs) ys with
      | ⟨dy, property_1⟩ =>
        match suffixLevenshtein C xs ys with
        | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))

Tactic:
conv =>
  lhs
  dsimp only [suffixLevenshtein_cons₂]

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (impl C (x :: xs) y (suffixLevenshtein C (x :: xs) ys)).val[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | ⟨dx, property⟩ =>
      match suffixLevenshtein C (x :: xs) ys with
      | ⟨dy, property_1⟩ =>
        match suffixLevenshtein C xs ys with
        | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (impl C (x :: xs) y ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩).val[0] =
    min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0])
      (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0])
        (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))

Tactic:
rw [impl_cons_fst_zero]

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ (match impl C xs y ⟨(suffixLevenshtein C xs ys).val, ?w'⟩ with
    | ⟨r, w⟩ =>
      min (C.delete x + r[0])
        (min (C.insert y + levenshtein C (x :: xs) ys) (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))) =
    min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0])
      (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0])
        (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))

case w'
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length
⊢ 0 < (suffixLevenshtein C xs ys).val.length