-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_length (xs : List α) (ys : List β) :
    (suffixLevenshtein C xs ys).1.length = xs.length + 1

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : (suffixLevenshtein C xs ys).val.length = xs.length + 1
⊢ (suffixLevenshtein C xs (y :: ys)).val.length = xs.length + 1

Tactic:
dsimp [suffixLevenshtein]

Result:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : (suffixLevenshtein C xs ys).val.length = xs.length + 1
⊢ (impl C xs y
          (List.foldr (impl C xs)
            (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs)
            ys)).val.length =
    xs.length + 1

Proof state:
case nil.nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ []).val.length =
    [].length + 1

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 α β δ
xs : List α
y : β
ys : List β
ih : (suffixLevenshtein C xs ys).val.length = xs.length + 1
⊢ (List.foldr (impl C xs)
          (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs)
          ys).val.length =
    xs.length + 1

Tactic:
exact ih

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs).val.length =
    xs.length + 1

Tactic:
induction xs with
| nil => rfl
| cons _ xs ih =>
  simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ (suffixLevenshtein C xs []).val.length = xs.length + 1

Tactic:
dsimp [suffixLevenshtein]

Result:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs).val.length =
    xs.length + 1

Proof state:
case nil.cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
head✝ : α
xs : List α
ih :
  (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs).val.length =
    xs.length + 1
⊢ (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩
          (head✝ :: xs)).val.length =
    (head✝ :: xs).length + 1

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : (suffixLevenshtein C xs ys).val.length = xs.length + 1
⊢ (impl C xs y
          (List.foldr (impl C xs)
            (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs)
            ys)).val.length =
    xs.length + 1

Tactic:
rw [impl_length]

Result:
case cons.w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : (suffixLevenshtein C xs ys).val.length = xs.length + 1
⊢ (List.foldr (impl C xs)
          (List.foldr (fun a x => ⟨(C.delete a + x.val[0]) :: x.val, ⋯⟩) ⟨[0], suffixLevenshtein.proof_2⟩ xs)
          ys).val.length =
    xs.length + 1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
⊢ (suffixLevenshtein C xs ys).val.length = xs.length + 1

Tactic:
induction ys with
| nil =>
  dsimp [suffixLevenshtein]
  induction xs with
  | nil => rfl
  | cons _ xs ih =>
    simp_all
| cons y ys ih =>
  dsimp [suffixLevenshtein]
  rw [impl_length]
  exact ih

Result:
no goals