-- Mathlib/Data/List/EditDistance/Defs.lean
theorem impl_length (d : {r : List δ // 0 < r.length}) (w : d.1.length = xs.length + 1) :
    (impl C xs y d).1.length = xs.length + 1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ 0 < (d₂ :: ds).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
d : { r // 0 < r.length }
w : d.val.length = xs.length + 1
⊢ (impl C xs y d).val.length = xs.length + 1

Tactic:
induction xs generalizing d with
| nil => rfl
| cons x xs ih =>
  dsimp [impl]
  match d, w with
  | ⟨d₁ :: d₂ :: ds, _⟩, w =>
    dsimp
    congr 1
    exact ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs : List α
y : β
d : { r // 0 < r.length }
w : d.val.length = [].length + 1
⊢ (impl C [] y d).val.length = [].length + 1

Tactic:
rfl

Result:
no goals

Proof state:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ (List.foldr
          (fun x x_1 =>
            ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) :: x_1.val,
              ⋯⟩)
          ⟨[C.insert y + (d₁ :: d₂ :: ds).getLast ⋯], impl.proof_3⟩ (xs.zip ((d₂ :: ds).zip ds))).val.length =
    xs.length + 1

Tactic:
exact ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)

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 : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w : d.val.length = (x :: xs).length + 1
⊢ (List.foldr
          (fun x x_1 =>
            ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) :: x_1.val,
              ⋯⟩)
          ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩ ((x :: xs).zip (d.val.zip d.val.tail))).val.length =
    xs.length + 1 + 1

Tactic:
match d, w with
| ⟨d₁ :: d₂ :: ds, _⟩, w =>
  dsimp
  congr 1
  exact ih ⟨d₂ :: ds, (by simp)⟩ (by simpa using w)

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 : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w : d.val.length = (x :: xs).length + 1
⊢ (impl C (x :: xs) y d).val.length = (x :: xs).length + 1

Tactic:
dsimp [impl]

Result:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w : d.val.length = (x :: xs).length + 1
⊢ (List.foldr
          (fun x x_1 =>
            ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) :: x_1.val,
              ⋯⟩)
          ⟨[C.insert y + d.val.getLast ⋯], impl.proof_3⟩ ((x :: xs).zip (d.val.zip d.val.tail))).val.length =
    xs.length + 1 + 1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ (List.foldr
          (fun x x_1 =>
            ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) :: x_1.val,
              ⋯⟩)
          ⟨[C.insert y + ⟨d₁ :: d₂ :: ds, property✝⟩.val.getLast ⋯], impl.proof_3⟩
          ((x :: xs).zip (⟨d₁ :: d₂ :: ds, property✝⟩.val.zip ⟨d₁ :: d₂ :: ds, property✝⟩.val.tail))).val.length =
    xs.length + 1 + 1

Tactic:
dsimp

Result:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ (List.foldr
            (fun x x_1 =>
              ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) ::
                  x_1.val,
                ⋯⟩)
            ⟨[C.insert y + (d₁ :: d₂ :: ds).getLast ⋯], impl.proof_3⟩ (xs.zip ((d₂ :: ds).zip ds))).val.length +
      1 =
    xs.length + 1 + 1

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ ⟨d₂ :: ds, ⋯⟩.val.length = xs.length + 1

Tactic:
simpa using w

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ (List.foldr
            (fun x x_1 =>
              ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) ::
                  x_1.val,
                ⋯⟩)
            ⟨[C.insert y + (d₁ :: d₂ :: ds).getLast ⋯], impl.proof_3⟩ (xs.zip ((d₂ :: ds).zip ds))).val.length +
      1 =
    xs.length + 1 + 1

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
xs✝ : List α
y : β
x : α
xs : List α
ih : ∀ (d : { r // 0 < r.length }), d.val.length = xs.length + 1 → (impl C xs y d).val.length = xs.length + 1
d : { r // 0 < r.length }
w✝ : d.val.length = (x :: xs).length + 1
d₁ d₂ : δ
ds : List δ
property✝ : 0 < (d₁ :: d₂ :: ds).length
w : ⟨d₁ :: d₂ :: ds, property✝⟩.val.length = (x :: xs).length + 1
⊢ (List.foldr
          (fun x x_1 =>
            ⟨min (C.delete x.fst + x_1.val[0]) (min (C.insert y + x.2.fst) (C.substitute x.fst y + x.2.snd)) :: x_1.val,
              ⋯⟩)
          ⟨[C.insert y + (d₁ :: d₂ :: ds).getLast ⋯], impl.proof_3⟩ (xs.zip ((d₂ :: ds).zip ds))).val.length =
    xs.length + 1