-- Mathlib/Data/List/EditDistance/Bounds.lean
theorem suffixLevenshtein_minimum_le_levenshtein_cons (xs : List α) (y ys) :
    (suffixLevenshtein C xs ys).1.minimum ≤ levenshtein C xs (y :: ys)

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.delete x + levenshtein C xs (y :: ys)) ∧
    (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.insert y + levenshtein C (x :: xs) ys) ∧
      (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.substitute x y + levenshtein C xs ys)

Tactic:
refine ⟨?_, ?_, ?_⟩

Result:
case cons.refine_1
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.delete x + levenshtein C xs (y :: ys))

case cons.refine_2
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.insert y + levenshtein C (x :: xs) ys)

case cons.refine_3
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(C.substitute x y + levenshtein C xs ys)

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ ↑(levenshtein C xs (y :: ys)) ≤ ↑(C.delete x + levenshtein C xs (y :: ys))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
⊢ 0 ≤ C.insert y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ ↑(levenshtein C xs ys) ≤ ↑(C.substitute x y + levenshtein C xs ys)

Tactic:
simp

Result:
no goals

Proof state:
case a.cons
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x head✝ : α
tail✝ : List α
ih : (↑(suffixLevenshtein C (head✝ :: tail✝) ys)).minimum ≤ ↑(levenshtein C (head✝ :: tail✝) (y :: ys))
⊢ (↑(suffixLevenshtein C (head✝ :: tail✝) ys)).minimum ≤ ↑(levenshtein C (head✝ :: tail✝) ys)

Tactic:
simp [suffixLevenshtein_cons₁, List.minimum_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
xs : List α
ih : (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ (↑(suffixLevenshtein C xs ys)).minimum

Tactic:
simp [suffixLevenshtein_cons₁_fst, List.minimum_cons]

Result:
no goals

Proof state:
case a.nil
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
x : α
ih : (↑(suffixLevenshtein C [] ys)).minimum ≤ ↑(levenshtein C [] (y :: ys))
⊢ (↑(suffixLevenshtein C [] ys)).minimum ≤ ↑(levenshtein C [] ys)

Tactic:
simp [suffixLevenshtein_nil']

Result:
no goals