-- Mathlib/Data/List/EditDistance/Defs.lean
theorem levenshtein_nil_cons (y) (ys) :
    levenshtein C [] (y :: ys) = C.insert y + levenshtein C [] ys

Proof state:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val.getLast
      ⋯ =
    (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]

Tactic:
rw [List.getLast_eq_getElem]

Result:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
          ys).val[(List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩)
              ⟨[0], suffixLevenshtein.proof_2⟩ ys).val.length -
        1] =
    (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ levenshtein C [] (y :: ys) = C.insert y + levenshtein C [] ys

Tactic:
dsimp (config := { unfoldPartialApp := true }) [levenshtein, suffixLevenshtein, impl]

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ C.insert y +
      (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
              ys).val.getLast
        ⋯ =
    C.insert y +
      (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val[0]

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
          ys).val.length =
    1

Tactic:
induction ys <;> simp

Result:
no goals

Proof state:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
          ys).val[(List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩)
              ⟨[0], suffixLevenshtein.proof_2⟩ ys).val.length -
        1] =
    (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]

Tactic:
congr

Result:
case e_a.e_i
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val.length -
      1 =
    0

Proof state:
case e_a.e_i
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val.length -
      1 =
    0

Tactic:
rw [show (List.length _) = 1 from _]

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
          ys).val.length =
    1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ C.insert y +
      (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
              ys).val.getLast
        ⋯ =
    C.insert y +
      (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val[0]

Tactic:
congr

Result:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩
            ys).val.getLast
      ⋯ =
    (List.foldr (fun y d => ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩) ⟨[0], suffixLevenshtein.proof_2⟩ ys).val[0]