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

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))

Tactic:
refine (?_ : _ ≤ _).trans (suffixLevenshtein_minimum_le_levenshtein_cons _ _ _)

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ (↑(suffixLevenshtein C a ys)).minimum

Proof state:
case h.h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
b : δ
m : b ∈ List.map (fun xs' => levenshtein C xs' ys) a.tails
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑b

Tactic:
replace m : ∃ a_1, a_1 <:+ a ∧ levenshtein C a_1 ys = b := by simpa using m

Result:
case h.h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
b : δ
m : ∃ a_1, a_1 <:+ a ∧ levenshtein C a_1 ys = b
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑b

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
b : δ
m : b ∈ List.map (fun xs' => levenshtein C xs' ys) a.tails
⊢ ∃ a_1, a_1 <:+ a ∧ levenshtein C a_1 ys = b

Tactic:
simpa using m

Result:
no goals

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

Tactic:
apply List.le_minimum_of_forall_le

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : δ), a ∈ ↑(suffixLevenshtein C xs (y :: ys)) → (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑a

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : List α),
    a <:+ xs → (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))

Tactic:
intro a suff

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ (↑(suffixLevenshtein C a ys)).minimum

Tactic:
simp only [suffixLevenshtein_eq_tails_map]

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤
    (List.map (fun xs' => levenshtein C xs' ys) a.tails).minimum

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤
    (List.map (fun xs' => levenshtein C xs' ys) a.tails).minimum

Tactic:
apply List.le_minimum_of_forall_le

Result:
case h.h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
⊢ ∀ (a_1 : δ),
    a_1 ∈ List.map (fun xs' => levenshtein C xs' ys) a.tails →
      (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑a_1

Proof state:
case h.h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
b : δ
m : ∃ a_1, a_1 <:+ a ∧ levenshtein C a_1 ys = b
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑b

Tactic:
obtain ⟨a', suff', rfl⟩ := m

Result:
case h.h.intro.intro
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
a' : List α
suff' : a' <:+ a
⊢ (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a' ys)

Proof state:
case h.h.intro.intro.ha
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
a' : List α
suff' : a' <:+ a
⊢ ∃ a, a <:+ xs ∧ levenshtein C a ys = levenshtein C a' ys

Tactic:
exact ⟨a', suff'.trans suff, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
a : List α
suff : a <:+ xs
a' : List α
suff' : a' <:+ a
this : ∃ a, a <:+ xs ∧ levenshtein C a ys = levenshtein C a' ys
⊢ ∃ a, a <:+ xs ∧ levenshtein C a ys = levenshtein C a' ys

Tactic:
simpa

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : δ), a ∈ ↑(suffixLevenshtein C xs (y :: ys)) → (↑(suffixLevenshtein C xs ys)).minimum ≤ ↑a

Tactic:
simp only [suffixLevenshtein_eq_tails_map]

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : δ),
    a ∈ List.map (fun xs' => levenshtein C xs' (y :: ys)) xs.tails →
      (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑a

Proof state:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : δ),
    a ∈ List.map (fun xs' => levenshtein C xs' (y :: ys)) xs.tails →
      (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑a

Tactic:
simp only [List.mem_map, List.mem_tails, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
case h
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
y : β
ys : List β
⊢ ∀ (a : List α),
    a <:+ xs → (List.map (fun xs' => levenshtein C xs' ys) xs.tails).minimum ≤ ↑(levenshtein C a (y :: ys))