[GOAL]
α : Type ?u.1129
β : Type ?u.1132
δ : Type ?u.1135
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
d : { r // 0 < List.length r }
ds : List δ
w✝ : 0 < List.length ds
x✝¹ : α × δ × δ
x✝ : { r // 0 < List.length r }
x : α
d₀ d₁ : δ
r : List δ
w : 0 < List.length r
⊢ 0 < List.length (min (Cost.delete C x + r[0]) (min (Cost.insert C y + d₀) (Cost.substitute C x y + d₁)) :: r)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.1129
β : Type ?u.1132
δ : Type ?u.1135
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
d : { r // 0 < List.length r }
ds : List δ
w : 0 < List.length ds
⊢ 0 < List.length [Cost.insert C y + List.getLast ds (_ : ds ≠ [])]
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.4624
β : Type ?u.4627
δ : Type ?u.4630
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d : δ
ds : List δ
w✝ : 0 < List.length (d :: ds)
w' : 0 < List.length ds
r : List δ
w : 0 < List.length r
⊢ 0 < List.length (min (Cost.delete C x + r[0]) (min (Cost.insert C y + d) (Cost.substitute C x y + ds[0])) :: r)
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
d : { r // 0 < List.length r }
w : List.length ↑d = List.length xs + 1
⊢ List.length ↑(impl C xs y d) = List.length xs + 1
[PROOFSTEP]
induction xs generalizing d
[GOAL]
case nil
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
d : { r // 0 < List.length r }
w : List.length ↑d = List.length [] + 1
⊢ List.length ↑(impl C [] y d) = List.length [] + 1
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
d : { r // 0 < List.length r }
w : List.length ↑d = List.length [] + 1
⊢ List.length ↑(impl C [] y d) = List.length [] + 1
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
d : { r // 0 < List.length r }
w : List.length ↑d = List.length [] + 1
⊢ List.length ↑(impl C [] y d) = List.length [] + 1
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length tail✝ + 1 → List.length ↑(impl C tail✝ y d) = List.length tail✝ + 1
d : { r // 0 < List.length r }
w : List.length ↑d = List.length (head✝ :: tail✝) + 1
⊢ List.length ↑(impl C (head✝ :: tail✝) y d) = List.length (head✝ :: tail✝) + 1
[PROOFSTEP]
case cons x xs ih =>
  dsimp [impl]
  match d, w with
  | ⟨d₁ :: d₂ :: ds, _⟩, w =>
    dsimp
    congr 1
    refine ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w : List.length ↑d = List.length (x :: xs) + 1
⊢ List.length ↑(impl C (x :: xs) y d) = List.length (x :: xs) + 1
[PROOFSTEP]
case cons x xs ih =>
  dsimp [impl]
  match d, w with
  | ⟨d₁ :: d₂ :: ds, _⟩, w =>
    dsimp
    congr 1
    refine ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w : List.length ↑d = List.length (x :: xs) + 1
⊢ List.length ↑(impl C (x :: xs) y d) = List.length (x :: xs) + 1
[PROOFSTEP]
dsimp [impl]
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds : List δ
w✝ : 0 < List.length (d✝ :: ds)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w : List.length ↑d = List.length (x :: xs) + 1
⊢ List.length
      ↑(List.foldr
          (fun x x_1 =>
            {
              val :=
                min (Cost.delete C x.fst + List.get ↑x_1 { val := 0, isLt := (_ : 0 < List.length ↑x_1) })
                    (min (Cost.insert C y + x.2.fst) (Cost.substitute C x.fst y + x.2.snd)) ::
                  ↑x_1,
              property := (_ : 0 < Nat.succ (List.length ↑x_1)) })
          { val := [Cost.insert C y + List.getLast ↑d (_ : ↑d ≠ [])], property := impl.proof_3 }
          (List.zip (x :: xs) (List.zip (↑d) (List.tail ↑d)))) =
    Nat.succ (List.length xs) + 1
[PROOFSTEP]
match d, w with
| ⟨d₁ :: d₂ :: ds, _⟩, w =>
  dsimp
  congr 1
  refine ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds✝ : List δ
w✝¹ : 0 < List.length (d✝ :: ds✝)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w✝ : List.length ↑d = List.length (x :: xs) + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < List.length (d₁ :: d₂ :: ds)
w : List.length ↑{ val := d₁ :: d₂ :: ds, property := property✝ } = List.length (x :: xs) + 1
⊢ List.length
      ↑(List.foldr
          (fun x x_1 =>
            {
              val :=
                min (Cost.delete C x.fst + List.get ↑x_1 { val := 0, isLt := (_ : 0 < List.length ↑x_1) })
                    (min (Cost.insert C y + x.2.fst) (Cost.substitute C x.fst y + x.2.snd)) ::
                  ↑x_1,
              property := (_ : 0 < Nat.succ (List.length ↑x_1)) })
          {
            val :=
              [Cost.insert C y +
                  List.getLast ↑{ val := d₁ :: d₂ :: ds, property := property✝ }
                    (_ : ↑{ val := d₁ :: d₂ :: ds, property := property✝ } ≠ [])],
            property := impl.proof_3 }
          (List.zip (x :: xs)
            (List.zip (↑{ val := d₁ :: d₂ :: ds, property := property✝ })
              (List.tail ↑{ val := d₁ :: d₂ :: ds, property := property✝ })))) =
    Nat.succ (List.length xs) + 1
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds✝ : List δ
w✝¹ : 0 < List.length (d✝ :: ds✝)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w✝ : List.length ↑d = List.length (x :: xs) + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < List.length (d₁ :: d₂ :: ds)
w : List.length ↑{ val := d₁ :: d₂ :: ds, property := property✝ } = List.length (x :: xs) + 1
⊢ Nat.succ
      (List.length
        ↑(List.foldr
            (fun x x_1 =>
              {
                val :=
                  min (Cost.delete C x.fst + List.get ↑x_1 { val := 0, isLt := (_ : 0 < List.length ↑x_1) })
                      (min (Cost.insert C y + x.2.fst) (Cost.substitute C x.fst y + x.2.snd)) ::
                    ↑x_1,
                property := (_ : 0 < Nat.succ (List.length ↑x_1)) })
            { val := [Cost.insert C y + List.getLast (d₁ :: d₂ :: ds) (_ : d₁ :: d₂ :: ds ≠ [])],
              property := impl.proof_3 }
            (List.zipWith Prod.mk xs (List.zipWith Prod.mk (d₂ :: ds) ds)))) =
    Nat.succ (List.length xs) + 1
[PROOFSTEP]
congr 1
[GOAL]
case e_n
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds✝ : List δ
w✝¹ : 0 < List.length (d✝ :: ds✝)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w✝ : List.length ↑d = List.length (x :: xs) + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < List.length (d₁ :: d₂ :: ds)
w : List.length ↑{ val := d₁ :: d₂ :: ds, property := property✝ } = List.length (x :: xs) + 1
⊢ List.length
      ↑(List.foldr
          (fun x x_1 =>
            {
              val :=
                min (Cost.delete C x.fst + List.get ↑x_1 { val := 0, isLt := (_ : 0 < List.length ↑x_1) })
                    (min (Cost.insert C y + x.2.fst) (Cost.substitute C x.fst y + x.2.snd)) ::
                  ↑x_1,
              property := (_ : 0 < Nat.succ (List.length ↑x_1)) })
          { val := [Cost.insert C y + List.getLast (d₁ :: d₂ :: ds) (_ : d₁ :: d₂ :: ds ≠ [])],
            property := impl.proof_3 }
          (List.zipWith Prod.mk xs (List.zipWith Prod.mk (d₂ :: ds) ds))) =
    List.length xs + 1
[PROOFSTEP]
refine ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds✝ : List δ
w✝¹ : 0 < List.length (d✝ :: ds✝)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w✝ : List.length ↑d = List.length (x :: xs) + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < List.length (d₁ :: d₂ :: ds)
w : List.length ↑{ val := d₁ :: d₂ :: ds, property := property✝ } = List.length (x :: xs) + 1
⊢ 0 < List.length (d₂ :: ds)
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x✝ : α
xs✝ : List α
y : β
d✝ : δ
ds✝ : List δ
w✝¹ : 0 < List.length (d✝ :: ds✝)
x : α
xs : List α
ih :
  ∀ (d : { r // 0 < List.length r }),
    List.length ↑d = List.length xs + 1 → List.length ↑(impl C xs y d) = List.length xs + 1
d : { r // 0 < List.length r }
w✝ : List.length ↑d = List.length (x :: xs) + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < List.length (d₁ :: d₂ :: ds)
w : List.length ↑{ val := d₁ :: d₂ :: ds, property := property✝ } = List.length (x :: xs) + 1
⊢ List.length ↑{ val := d₂ :: ds, property := (_ : 0 < Nat.succ (List.length ds)) } = List.length xs + 1
[PROOFSTEP]
simpa using w
[GOAL]
α : Type ?u.20925
β : Type ?u.20928
δ : Type ?u.20931
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
a : α
x✝ : { r // 0 < List.length r }
r : List δ
w : 0 < List.length r
⊢ 0 < List.length ((Cost.delete C a + r[0]) :: r)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.20925
β : Type ?u.20928
δ : Type ?u.20931
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
⊢ 0 < List.length [0]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
⊢ List.length ↑(suffixLevenshtein C xs ys) = List.length xs + 1
[PROOFSTEP]
induction ys
[GOAL]
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ List.length ↑(suffixLevenshtein C xs []) = List.length xs + 1
[PROOFSTEP]
case nil =>
  dsimp [suffixLevenshtein]
  induction xs
  · case nil => rfl
  · case cons _ xs ih => simp_all
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ List.length ↑(suffixLevenshtein C xs []) = List.length xs + 1
[PROOFSTEP]
case nil =>
  dsimp [suffixLevenshtein]
  induction xs
  · case nil => rfl
  · case cons _ xs ih => simp_all
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ List.length ↑(suffixLevenshtein C xs []) = List.length xs + 1
[PROOFSTEP]
dsimp [suffixLevenshtein]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } xs) =
    List.length xs + 1
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } []) =
    List.length [] + 1
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } []) =
    List.length [] + 1
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } []) =
    List.length [] + 1
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } tail✝) =
    List.length tail✝ + 1
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } (head✝ :: tail✝)) =
    List.length (head✝ :: tail✝) + 1
[PROOFSTEP]
case cons _ xs ih => simp_all
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
head✝ : α
xs : List α
ih :
  List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } xs) =
    List.length xs + 1
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } (head✝ :: xs)) =
    List.length (head✝ :: xs) + 1
[PROOFSTEP]
case cons _ xs ih => simp_all
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
head✝ : α
xs : List α
ih :
  List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } xs) =
    List.length xs + 1
⊢ List.length
      ↑(List.foldr
          (fun a x =>
            { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
              property := (_ : 0 < Nat.succ (List.length ↑x)) })
          { val := [0], property := suffixLevenshtein.proof_2 } (head✝ :: xs)) =
    List.length (head✝ :: xs) + 1
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
head✝ : β
tail✝ : List β
tail_ih✝ : List.length ↑(suffixLevenshtein C xs tail✝) = List.length xs + 1
⊢ List.length ↑(suffixLevenshtein C xs (head✝ :: tail✝)) = List.length xs + 1
[PROOFSTEP]
case cons y ys ih =>
  dsimp [suffixLevenshtein]
  rw [impl_length]
  exact ih
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : List.length ↑(suffixLevenshtein C xs ys) = List.length xs + 1
⊢ List.length ↑(suffixLevenshtein C xs (y :: ys)) = List.length xs + 1
[PROOFSTEP]
case cons y ys ih =>
  dsimp [suffixLevenshtein]
  rw [impl_length]
  exact ih
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : List.length ↑(suffixLevenshtein C xs ys) = List.length xs + 1
⊢ List.length ↑(suffixLevenshtein C xs (y :: ys)) = List.length xs + 1
[PROOFSTEP]
dsimp [suffixLevenshtein]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : List.length ↑(suffixLevenshtein C xs ys) = List.length xs + 1
⊢ List.length
      ↑(impl C xs y
          (List.foldr (impl C xs)
            (List.foldr
              (fun a x =>
                { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
                  property := (_ : 0 < Nat.succ (List.length ↑x)) })
              { val := [0], property := suffixLevenshtein.proof_2 } xs)
            ys)) =
    List.length xs + 1
[PROOFSTEP]
rw [impl_length]
[GOAL]
case w
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
ih : List.length ↑(suffixLevenshtein C xs ys) = List.length xs + 1
⊢ List.length
      ↑(List.foldr (impl C xs)
          (List.foldr
            (fun a x =>
              { val := (Cost.delete C a + List.get ↑x { val := 0, isLt := (_ : 0 < List.length ↑x) }) :: ↑x,
                property := (_ : 0 < Nat.succ (List.length ↑x)) })
            { val := [0], property := suffixLevenshtein.proof_2 } xs)
          ys) =
    List.length xs + 1
[PROOFSTEP]
exact ih
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
ys : List β
⊢ impl C xs y (suffixLevenshtein C xs ys) = suffixLevenshtein C xs (y :: ys)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ ↑(suffixLevenshtein C [] []) = [0]
[PROOFSTEP]
rfl
  -- Not sure if this belongs in the main `List` API, or can stay local.
[GOAL]
α : Type u_1
β : Type ?u.25854
δ : Type ?u.25857
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : List α
w : length x = 1
⊢ let_fun this := (_ : 0 < length x);
  x = [x[0]]
[PROOFSTEP]
match x, w with
| [r], _ => rfl
[GOAL]
α : Type u_1
β : Type ?u.25854
δ : Type ?u.25857
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : List α
w : length x = 1
r : α
x✝ : length [r] = 1
⊢ let_fun this := (_ : 0 < length [r]);
  [r] = [[r][0]]
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.27296
β : Type ?u.27299
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x y : { r // 0 < List.length r }
w₀ : (↑x)[0] = (↑y)[0]
w : List.tail ↑x = List.tail ↑y
⊢ x = y
[PROOFSTEP]
match x, y with
| ⟨hx :: tx, _⟩, ⟨hy :: ty, _⟩ => simp_all
[GOAL]
α : Type ?u.27296
β : Type ?u.27299
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x y : { r // 0 < List.length r }
hx : δ
tx : List δ
property✝¹ : 0 < List.length (hx :: tx)
hy : δ
ty : List δ
property✝ : 0 < List.length (hy :: ty)
w₀ : (↑{ val := hx :: tx, property := property✝¹ })[0] = (↑{ val := hy :: ty, property := property✝ })[0]
w : List.tail ↑{ val := hx :: tx, property := property✝¹ } = List.tail ↑{ val := hy :: ty, property := property✝ }
⊢ { val := hx :: tx, property := property✝¹ } = { val := hy :: ty, property := property✝ }
[PROOFSTEP]
simp_all
[GOAL]
α : Type ?u.29177
β : Type ?u.29180
δ : Type ?u.29183
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
ys : List β
⊢ 0 < List.length (levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
ys : List β
⊢ suffixLevenshtein C (x :: xs) ys =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
[PROOFSTEP]
induction ys
[GOAL]
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
⊢ suffixLevenshtein C (x :: xs) [] =
    { val := levenshtein C (x :: xs) [] :: ↑(suffixLevenshtein C xs []),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs []))) }
[PROOFSTEP]
case nil => dsimp [levenshtein, suffixLevenshtein]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
⊢ suffixLevenshtein C (x :: xs) [] =
    { val := levenshtein C (x :: xs) [] :: ↑(suffixLevenshtein C xs []),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs []))) }
[PROOFSTEP]
case nil => dsimp [levenshtein, suffixLevenshtein]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
⊢ suffixLevenshtein C (x :: xs) [] =
    { val := levenshtein C (x :: xs) [] :: ↑(suffixLevenshtein C xs []),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs []))) }
[PROOFSTEP]
dsimp [levenshtein, suffixLevenshtein]
[GOAL]
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
head✝ : β
tail✝ : List β
tail_ih✝ :
  suffixLevenshtein C (x :: xs) tail✝ =
    { val := levenshtein C (x :: xs) tail✝ :: ↑(suffixLevenshtein C xs tail✝),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs tail✝))) }
⊢ suffixLevenshtein C (x :: xs) (head✝ :: tail✝) =
    { val := levenshtein C (x :: xs) (head✝ :: tail✝) :: ↑(suffixLevenshtein C xs (head✝ :: tail✝)),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (head✝ :: tail✝)))) }
[PROOFSTEP]
case cons y ys ih =>
  apply suffixLevenshtein_cons₁_aux
  · rfl
  · rw [suffixLevenshtein_cons₂ (x :: xs), ih, impl_cons]
    · rfl
    · simp [suffixLevenshtein_length]
[GOAL]
α : 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ suffixLevenshtein C (x :: xs) (y :: ys) =
    { val := levenshtein C (x :: xs) (y :: ys) :: ↑(suffixLevenshtein C xs (y :: ys)),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (y :: ys)))) }
[PROOFSTEP]
case cons y ys ih =>
  apply suffixLevenshtein_cons₁_aux
  · rfl
  · rw [suffixLevenshtein_cons₂ (x :: xs), ih, impl_cons]
    · rfl
    · simp [suffixLevenshtein_length]
[GOAL]
α : 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ suffixLevenshtein C (x :: xs) (y :: ys) =
    { val := levenshtein C (x :: xs) (y :: ys) :: ↑(suffixLevenshtein C xs (y :: ys)),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (y :: ys)))) }
[PROOFSTEP]
apply suffixLevenshtein_cons₁_aux
[GOAL]
case 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0] =
    (↑{ val := levenshtein C (x :: xs) (y :: ys) :: ↑(suffixLevenshtein C xs (y :: ys)),
          property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (y :: ys)))) })[0]
[PROOFSTEP]
rfl
[GOAL]
case 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ List.tail ↑(suffixLevenshtein C (x :: xs) (y :: ys)) =
    List.tail
      ↑{ val := levenshtein C (x :: xs) (y :: ys) :: ↑(suffixLevenshtein C xs (y :: ys)),
          property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (y :: ys)))) }
[PROOFSTEP]
rw [suffixLevenshtein_cons₂ (x :: xs), ih, impl_cons]
[GOAL]
case 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ List.tail
      ↑(match impl C xs y { val := ↑(suffixLevenshtein C xs ys), property := ?w.w' } with
        | { val := r, property := w } =>
          {
            val :=
              min (Cost.delete C x + r[0])
                  (min (Cost.insert C y + levenshtein C (x :: xs) ys)
                    (Cost.substitute C x y + (↑(suffixLevenshtein C xs ys))[0])) ::
                r,
            property := (_ : 0 < Nat.succ (List.length r)) }) =
    List.tail
      ↑{ val := levenshtein C (x :: xs) (y :: ys) :: ↑(suffixLevenshtein C xs (y :: ys)),
          property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs (y :: ys)))) }
[PROOFSTEP]
rfl
[GOAL]
case 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 =
    { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
      property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }
⊢ 0 < List.length ↑(suffixLevenshtein C xs ys)
[PROOFSTEP]
simp [suffixLevenshtein_length]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
ys : List β
⊢ ↑(suffixLevenshtein C (x :: xs) ys) = levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys)
[PROOFSTEP]
simp [suffixLevenshtein_cons₁]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
⊢ (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | { val := dx, property := property } =>
      match suffixLevenshtein C (x :: xs) ys with
      | { val := dy, property := property_1 } =>
        match suffixLevenshtein C xs ys with
        | { val := dxy, property := property_2 } =>
          min (Cost.delete C x + dx[0]) (min (Cost.insert C y + dy[0]) (Cost.substitute C x y + dxy[0]))
[PROOFSTEP]
conv =>
  lhs
  dsimp only [suffixLevenshtein_cons₂]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
| (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | { val := dx, property := property } =>
      match suffixLevenshtein C (x :: xs) ys with
      | { val := dy, property := property_1 } =>
        match suffixLevenshtein C xs ys with
        | { val := dxy, property := property_2 } =>
          min (Cost.delete C x + dx[0]) (min (Cost.insert C y + dy[0]) (Cost.substitute C x y + dxy[0]))
[PROOFSTEP]
  lhs
  dsimp only [suffixLevenshtein_cons₂]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
| (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | { val := dx, property := property } =>
      match suffixLevenshtein C (x :: xs) ys with
      | { val := dy, property := property_1 } =>
        match suffixLevenshtein C xs ys with
        | { val := dxy, property := property_2 } =>
          min (Cost.delete C x + dx[0]) (min (Cost.insert C y + dy[0]) (Cost.substitute C x y + dxy[0]))
[PROOFSTEP]
  lhs
  dsimp only [suffixLevenshtein_cons₂]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
| (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | { val := dx, property := property } =>
      match suffixLevenshtein C (x :: xs) ys with
      | { val := dy, property := property_1 } =>
        match suffixLevenshtein C xs ys with
        | { val := dxy, property := property_2 } =>
          min (Cost.delete C x + dx[0]) (min (Cost.insert C y + dy[0]) (Cost.substitute C x y + dxy[0]))
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
| (↑(suffixLevenshtein C (x :: xs) (y :: ys)))[0]
[PROOFSTEP]
dsimp only [suffixLevenshtein_cons₂]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
⊢ (↑(impl C (x :: xs) y (suffixLevenshtein C (x :: xs) ys)))[0] =
    match suffixLevenshtein C xs (y :: ys) with
    | { val := dx, property := property } =>
      match suffixLevenshtein C (x :: xs) ys with
      | { val := dy, property := property_1 } =>
        match suffixLevenshtein C xs ys with
        | { val := dxy, property := property_2 } =>
          min (Cost.delete C x + dx[0]) (min (Cost.insert C y + dy[0]) (Cost.substitute C x y + dxy[0]))
[PROOFSTEP]
simp only [suffixLevenshtein_cons₁]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
⊢ (↑(impl C (x :: xs) y
          { val := levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys),
            property := (_ : 0 < Nat.succ (List.length ↑(suffixLevenshtein C xs ys))) }))[0] =
    min (Cost.delete C x + (↑(suffixLevenshtein C xs (y :: ys)))[0])
      (min (Cost.insert C y + (levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys))[0])
        (Cost.substitute C x y + (↑(suffixLevenshtein C xs ys))[0]))
[PROOFSTEP]
rw [impl_cons_fst_zero]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
⊢ (match impl C xs y { val := ↑(suffixLevenshtein C xs ys), property := ?w' } with
    | { val := r, property := w } =>
      min (Cost.delete C x + r[0])
        (min (Cost.insert C y + levenshtein C (x :: xs) ys)
          (Cost.substitute C x y + (↑(suffixLevenshtein C xs ys))[0]))) =
    min (Cost.delete C x + (↑(suffixLevenshtein C xs (y :: ys)))[0])
      (min (Cost.insert C y + (levenshtein C (x :: xs) ys :: ↑(suffixLevenshtein C xs ys))[0])
        (Cost.substitute C x y + (↑(suffixLevenshtein C xs ys))[0]))
case w'
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
ys : List β
w : 0 < List.length ↑(suffixLevenshtein C (x :: xs) (y :: ys))
⊢ 0 < List.length ↑(suffixLevenshtein C xs ys)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
ys : List β
⊢ ↑(suffixLevenshtein C xs ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails xs)
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
⊢ ↑(suffixLevenshtein C [] ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails [])
[PROOFSTEP]
case nil => simp only [List.map, suffixLevenshtein_nil']
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
⊢ ↑(suffixLevenshtein C [] ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails [])
[PROOFSTEP]
case nil => simp only [List.map, suffixLevenshtein_nil']
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
⊢ ↑(suffixLevenshtein C [] ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails [])
[PROOFSTEP]
simp only [List.map, suffixLevenshtein_nil']
[GOAL]
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(suffixLevenshtein C tail✝ ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails tail✝)
⊢ ↑(suffixLevenshtein C (head✝ :: tail✝) ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails (head✝ :: tail✝))
[PROOFSTEP]
case cons x xs ih => simp only [List.map, suffixLevenshtein_cons₁, ih]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
x : α
xs : List α
ih : ↑(suffixLevenshtein C xs ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails xs)
⊢ ↑(suffixLevenshtein C (x :: xs) ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails (x :: xs))
[PROOFSTEP]
case cons x xs ih => simp only [List.map, suffixLevenshtein_cons₁, ih]
[GOAL]
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
ys : List β
x : α
xs : List α
ih : ↑(suffixLevenshtein C xs ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails xs)
⊢ ↑(suffixLevenshtein C (x :: xs) ys) = List.map (fun xs' => levenshtein C xs' ys) (List.tails (x :: xs))
[PROOFSTEP]
simp only [List.map, suffixLevenshtein_cons₁, ih]
[GOAL]
α : Type u_2
β : Type u_3
δ : Type u_1
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ levenshtein C [] [] = 0
[PROOFSTEP]
simp [levenshtein]
[GOAL]
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ levenshtein C [] (y :: ys) = Cost.insert C y + levenshtein C [] ys
[PROOFSTEP]
dsimp [levenshtein]
[GOAL]
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ Cost.insert C y +
      List.getLast ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys)
        (_ : ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) ≠ []) =
    Cost.insert C y +
      List.get ↑(suffixLevenshtein C [] ys) { val := 0, isLt := (_ : 0 < List.length ↑(suffixLevenshtein C [] ys)) }
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ List.getLast ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys)
      (_ : ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) ≠ []) =
    List.get ↑(suffixLevenshtein C [] ys) { val := 0, isLt := (_ : 0 < List.length ↑(suffixLevenshtein C [] ys)) }
[PROOFSTEP]
rw [List.getLast_eq_get]
[GOAL]
case e_a
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ List.get ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys)
      { val := List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) - 1,
        isLt :=
          (_ :
            List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) - 1 <
              List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys)) } =
    List.get ↑(suffixLevenshtein C [] ys) { val := 0, isLt := (_ : 0 < List.length ↑(suffixLevenshtein C [] ys)) }
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_val
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) - 1 = 0
[PROOFSTEP]
rw [show (List.length _) = 1 from _]
[GOAL]
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
[PROOFSTEP]
induction ys with
| nil => simp
| cons y ys ih =>
  simp only [List.foldr]
  rw [impl_length] <;> simp [ih]
[GOAL]
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
ys : List β
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
[PROOFSTEP]
induction ys with
| nil => simp
| cons y ys ih =>
  simp only [List.foldr]
  rw [impl_length] <;> simp [ih]
[GOAL]
case nil
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } []) = 1
[PROOFSTEP]

| nil => simp
[GOAL]
case nil
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y : β
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } []) = 1
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y✝ y : β
ys : List β
ih : List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } (y :: ys)) = 1
[PROOFSTEP]

| cons y ys ih =>
  simp only [List.foldr]
  rw [impl_length] <;> simp [ih]
[GOAL]
case cons
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y✝ y : β
ys : List β
ih : List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } (y :: ys)) = 1
[PROOFSTEP]
simp only [List.foldr]
[GOAL]
case cons
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y✝ y : β
ys : List β
ih : List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
⊢ List.length ↑(impl C [] y (List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys)) = 1
[PROOFSTEP]
rw [impl_length]
[GOAL]
case cons
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y✝ y : β
ys : List β
ih : List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
⊢ List.length [] + 1 = 1
[PROOFSTEP]
simp [ih]
[GOAL]
case cons.w
α : Type u_3
β : Type u_1
δ : Type u_2
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
y✝ y : β
ys : List β
ih : List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = 1
⊢ List.length ↑(List.foldr (impl C []) { val := [0], property := suffixLevenshtein.proof_2 } ys) = List.length [] + 1
[PROOFSTEP]
simp [ih]
