-- 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:
α : 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 ≤ ↑(levenshtein C xs ys)

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

Result:
α : 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 (x :: xs) ys) ⊓ (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs 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 ≤ ↑(levenshtein C (x :: xs) (y :: ys))

Tactic:
suffices
  (suffixLevenshtein C (x :: xs) ys).1.minimum ≤ (C.delete x + levenshtein C xs (y :: ys)) ∧
    (suffixLevenshtein C (x :: xs) ys).1.minimum ≤ (C.insert y + levenshtein C (x :: xs) ys) ∧
    (suffixLevenshtein C (x :: xs) ys).1.minimum ≤ (C.substitute x y + levenshtein C xs ys) by
  simpa [suffixLevenshtein_eq_tails_map]

Result:
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)

Proof state:
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))

Tactic:
calc
  _ ≤ (suffixLevenshtein C xs ys).1.minimum := by
      simp [suffixLevenshtein_cons₁_fst, List.minimum_cons]
  _ ≤ ↑(levenshtein C xs (y :: ys)) := ih
  _ ≤ _ := by 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))
this :
  (↑(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)
⊢ (↑(suffixLevenshtein C (x :: xs) ys)).minimum ≤ ↑(levenshtein C (x :: xs) (y :: ys))

Tactic:
simpa [suffixLevenshtein_eq_tails_map]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
⊢ levenshtein C [] ys ≤ C.insert y + levenshtein C [] ys

Tactic:
exact le_add_of_nonneg_left (by 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 (x :: xs) ys) ≤ ↑(C.insert y + levenshtein C (x :: xs) ys)

Tactic:
simp

Result:
no goals

Proof state:
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)

Tactic:
calc
  (suffixLevenshtein C (x :: xs) ys).1.minimum ≤ (levenshtein C (x :: xs) ys) := by
      simp [suffixLevenshtein_cons₁_fst, List.minimum_cons]
  _ ≤ _ := by simp

Result:
no goals

Proof state:
case a
α : 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 xs ys)).minimum ≤ ↑(levenshtein C xs ys)

Tactic:
cases xs

Result:
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)

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)

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 ≤ ↑(levenshtein C (x :: xs) ys)

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

Result:
no goals

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

Tactic:
simp only [suffixLevenshtein_nil', levenshtein_nil_cons,
  List.minimum_singleton, WithTop.coe_le_coe]

Result:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
y : β
ys : List β
⊢ levenshtein C [] ys ≤ C.insert y + levenshtein C [] 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 (x :: xs) ys) ⊓ (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs ys)

Tactic:
apply min_le_of_right_le

Result:
case a
α : 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 xs ys)).minimum ≤ ↑(levenshtein C xs ys)