-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_cons₁
    (x : α) (xs ys) :
    suffixLevenshtein C (x :: xs) ys =
      ⟨levenshtein C (x :: xs) ys ::
        (suffixLevenshtein C xs ys).1, by simp⟩

Proof state:
case cons.w₀
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (suffixLevenshtein C (x :: xs) (y :: ys)).val[0] =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val[0]

Tactic:
rfl

Result:
no goals

Proof state:
case cons.w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (suffixLevenshtein C (x :: xs) (y :: ys)).val.tail =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val.tail

Tactic:
rw [suffixLevenshtein_cons₂ (x :: xs), ih, impl_cons]

Result:
case cons.w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (match impl C xs y ⟨(suffixLevenshtein C xs ys).val, ?cons.w.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])) ::
              r,
            ⋯⟩).val.tail =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val.tail

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

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
⊢ suffixLevenshtein C (x :: xs) [] = ⟨levenshtein C (x :: xs) [] :: (suffixLevenshtein C xs []).val, ⋯⟩

Tactic:
dsimp [levenshtein, suffixLevenshtein]

Result:
no goals

Proof state:
case cons.w.w'
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ 0 < (suffixLevenshtein C xs ys).val.length

Tactic:
simp [suffixLevenshtein_length]

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ suffixLevenshtein C (x :: xs) (y :: ys) =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩

Tactic:
apply suffixLevenshtein_cons₁_aux

Result:
case cons.w₀
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (suffixLevenshtein C (x :: xs) (y :: ys)).val[0] =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val[0]

case cons.w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (suffixLevenshtein C (x :: xs) (y :: ys)).val.tail =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val.tail

Proof state:
case cons.w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
ih : suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
⊢ (match impl C xs y ⟨(suffixLevenshtein C xs ys).val, ?cons.w.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])) ::
              r,
            ⋯⟩).val.tail =
    ⟨levenshtein C (x :: xs) (y :: ys) :: (suffixLevenshtein C xs (y :: ys)).val, ⋯⟩.val.tail

Tactic:
rfl

Result:
no goals