[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]


[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ ↑card (disjSum s t) = ↑card s + ↑card t
[PROOFSTEP]
rw [disjSum, card_add, card_map, card_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ x ∈ disjSum s t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x
[PROOFSTEP]
simp_rw [disjSum, mem_add, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ inl a ∈ disjSum s t ↔ a ∈ s
[PROOFSTEP]
rw [mem_disjSum, or_iff_left]
  -- Porting note: Previous code for L62 was: simp only [exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ (∃ a_1, a_1 ∈ s ∧ inl a_1 = inl a) ↔ a ∈ s
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
[PROOFSTEP]
simp only [inl.injEq, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
[PROOFSTEP]
rintro ⟨b, _, hb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b✝ : β
x : α ⊕ β
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False
[PROOFSTEP]
exact inr_ne_inl hb
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ inr b ∈ disjSum s t ↔ b ∈ t
[PROOFSTEP]
rw [mem_disjSum, or_iff_right]
  -- Porting note: Previous code for L72 was: simp only [exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ (∃ b_1, b_1 ∈ t ∧ inr b_1 = inr b) ↔ b ∈ t
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
[PROOFSTEP]
simp only [inr.injEq, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
[PROOFSTEP]
rintro ⟨a, _, ha⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b : β
x : α ⊕ β
a : α
left✝ : a ∈ s
ha : inl a = inr b
⊢ False
[PROOFSTEP]
exact inl_ne_inr ha
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
hs : Nodup s
ht : Nodup t
⊢ Nodup (disjSum s t)
[PROOFSTEP]
refine' ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 fun x hs ht => _
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x✝ : α ⊕ β
hs✝ : Nodup s
ht✝ : Nodup t
x : α ⊕ β
hs : x ∈ Multiset.map inl s
ht : x ∈ Multiset.map inr t
⊢ False
[PROOFSTEP]
rw [Multiset.mem_map] at hs ht
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x✝ : α ⊕ β
hs✝ : Nodup s
ht✝ : Nodup t
x : α ⊕ β
hs : ∃ a, a ∈ s ∧ inl a = x
ht : ∃ a, a ∈ t ∧ inr a = x
⊢ False
[PROOFSTEP]
obtain ⟨a, _, rfl⟩ := hs
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b : β
x : α ⊕ β
hs : Nodup s
ht✝ : Nodup t
a : α
left✝ : a ∈ s
ht : ∃ a_1, a_1 ∈ t ∧ inr a_1 = inl a
⊢ False
[PROOFSTEP]
obtain ⟨b, _, h⟩ := ht
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b✝ : β
x : α ⊕ β
hs : Nodup s
ht : Nodup t
a : α
left✝¹ : a ∈ s
b : β
left✝ : b ∈ t
h : inr b = inl a
⊢ False
[PROOFSTEP]
exact inr_ne_inl h


[GOAL]
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ ~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
⊢ l₁ = l₂
[PROOFSTEP]
induction' s₁ with a l₁ h₁ s₁ IH generalizing l₂
[GOAL]
case nil
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
s₂✝ : Sorted r l₂✝
l₂ : List α
p : [] ~ l₂
s₂ : Sorted r l₂
⊢ [] = l₂
[PROOFSTEP]
exact p.nil_eq
[GOAL]
case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
⊢ a :: l₁ = l₂
[PROOFSTEP]
have : a ∈ l₂ := p.subset (mem_cons_self _ _)
[GOAL]
case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
this : a ∈ l₂
⊢ a :: l₁ = l₂
[PROOFSTEP]
rcases mem_split this with ⟨u₂, v₂, rfl⟩
[GOAL]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
[PROOFSTEP]
have p' := (perm_cons a).1 (p.trans perm_middle)
[GOAL]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
p' : l₁ ~ u₂ ++ v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
[PROOFSTEP]
obtain rfl := IH p' (s₂.sublist <| by simp)
[GOAL]
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
p' : l₁ ~ u₂ ++ v₂
⊢ u₂ ++ v₂ <+ u₂ ++ a :: v₂
[PROOFSTEP]
simp
[GOAL]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: (u₂ ++ v₂) = u₂ ++ a :: v₂
[PROOFSTEP]
change a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
[GOAL]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
[PROOFSTEP]
rw [← append_assoc]
[GOAL]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ [a] ++ v₂
[PROOFSTEP]
congr
[GOAL]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ = u₂ ++ [a]
[PROOFSTEP]
have : ∀ (x : α) (_ : x ∈ u₂), x = a := fun x m =>
  antisymm ((pairwise_append.1 s₂).2.2 _ m a (mem_cons_self _ _)) (h₁ _ (by simp [m]))
[GOAL]
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
x : α
m : x ∈ u₂
⊢ x ∈ u₂ ++ v₂
[PROOFSTEP]
simp [m]
[GOAL]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ a :: u₂ = u₂ ++ [a]
[PROOFSTEP]
rw [(@eq_replicate _ a (length u₂ + 1) (a :: u₂)).2, (@eq_replicate _ a (length u₂ + 1) (u₂ ++ [a])).2]
[GOAL]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ length (u₂ ++ [a]) = length u₂ + 1 ∧ ∀ (b : α), b ∈ u₂ ++ [a] → b = a
[PROOFSTEP]
constructor
[GOAL]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ length (a :: u₂) = length u₂ + 1 ∧ ∀ (b : α), b ∈ a :: u₂ → b = a
[PROOFSTEP]
constructor
[GOAL]
case cons.intro.intro.e_a.left
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ length (u₂ ++ [a]) = length u₂ + 1
[PROOFSTEP]
simp [iff_true_intro this, or_comm]
[GOAL]
case cons.intro.intro.e_a.right
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ ∀ (b : α), b ∈ u₂ ++ [a] → b = a
[PROOFSTEP]
simp [iff_true_intro this, or_comm]
[GOAL]
case cons.intro.intro.e_a.left
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ length (a :: u₂) = length u₂ + 1
[PROOFSTEP]
simp [iff_true_intro this, or_comm]
[GOAL]
case cons.intro.intro.e_a.right
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ ∀ (b : α), b ∈ a :: u₂ → b = a
[PROOFSTEP]
simp [iff_true_intro this, or_comm]
[GOAL]
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ <+~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
⊢ l₁ <+ l₂
[PROOFSTEP]
let ⟨_, h, h'⟩ := p
[GOAL]
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ <+~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂
[PROOFSTEP]
rwa [← eq_of_perm_of_sorted h (s₂.sublist h') s₁]
[GOAL]
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin (length l)
hab : a ≤ b
⊢ r (get l a) (get l b)
[PROOFSTEP]
rcases hab.eq_or_lt with (rfl | hlt)
[GOAL]
case inl
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a : Fin (length l)
hab : a ≤ a
⊢ r (get l a) (get l a)
case inr
α : Type uu
r : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : IsRefl α r
l : List α
h : Sorted r l
a b : Fin (length l)
hab : a ≤ b
hlt : a < b
⊢ r (get l a) (get l b)
[PROOFSTEP]
exacts [refl _, h.rel_get_of_lt hlt]
[GOAL]
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k : ℕ
x y : α
hx : x ∈ take k l
hy : y ∈ drop k l
⊢ r x y
[PROOFSTEP]
obtain ⟨⟨iy, hiy⟩, rfl⟩ := get_of_mem hy
[GOAL]
case intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k : ℕ
x : α
hx : x ∈ take k l
iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
⊢ r x (get (drop k l) { val := iy, isLt := hiy })
[PROOFSTEP]
obtain ⟨⟨ix, hix⟩, rfl⟩ := get_of_mem hx
[GOAL]
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get (take k l) { val := ix, isLt := hix }) (get (drop k l) { val := iy, isLt := hiy })
[PROOFSTEP]
rw [get_take', get_drop']
[GOAL]
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix : ix < length (take k l)
hx : get (take k l) { val := ix, isLt := hix } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix }, isLt := (_ : ↑{ val := ix, isLt := hix } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
[PROOFSTEP]
rw [length_take] at hix
[GOAL]
case intro.mk.intro.mk
α : Type uu
r : α → α → Prop
a : α
l✝ l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < length (drop k l)
hy : get (drop k l) { val := iy, isLt := hiy } ∈ drop k l
ix : ℕ
hix✝ : ix < length (take k l)
hix : ix < min k (length l)
hx : get (take k l) { val := ix, isLt := hix✝ } ∈ take k l
⊢ r (get l { val := ↑{ val := ix, isLt := hix✝ }, isLt := (_ : ↑{ val := ix, isLt := hix✝ } < length l) })
    (get l { val := k + ↑{ val := iy, isLt := hiy }, isLt := (_ : k + ↑{ val := iy, isLt := hiy } < length l) })
[PROOFSTEP]
exact h.rel_nthLe_of_lt _ _ (ix.lt_add_right _ _ (lt_min_iff.mp hix).left)
[GOAL]
n : ℕ
α : Type uu
inst✝ : Preorder α
f : Fin n → α
r : α → α → Prop
⊢ Sorted r (ofFn f) ↔ ((fun x x_1 => x < x_1) ⇒ r) f f
[PROOFSTEP]
simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]
[GOAL]
n : ℕ
α : Type uu
inst✝ : Preorder α
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i j : Fin (length (ofFn f))),
      i < j → r (f (↑(Fin.castIso (_ : length (ofFn f) = n)) i)) (f (↑(Fin.castIso (_ : length (ofFn f) = n)) j))) ↔
    ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)
[PROOFSTEP]
exact Iff.symm (Fin.castIso _).surjective.forall₂
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ length (orderedInsert r a (hd :: tl)) = length (hd :: tl) + 1
[PROOFSTEP]
dsimp [orderedInsert]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ length (if r a hd then a :: hd :: tl else hd :: orderedInsert r a tl) = Nat.succ (length tl) + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
h✝ : r a hd
⊢ length (a :: hd :: tl) = Nat.succ (length tl) + 1
[PROOFSTEP]
simp [orderedInsert_length tl]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
h✝ : ¬r a hd
⊢ length (hd :: orderedInsert r a tl) = Nat.succ (length tl) + 1
[PROOFSTEP]
simp [orderedInsert_length tl]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)
[PROOFSTEP]
dsimp only [orderedInsert]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ (if r a b then a :: b :: l else b :: orderedInsert r a l) =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ a :: b :: l = takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)
[PROOFSTEP]
simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ b :: orderedInsert r a l =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)
[PROOFSTEP]
simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
[PROOFSTEP]
by_cases h : a ≼ b
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
[PROOFSTEP]
simp [orderedInsert, h]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
[PROOFSTEP]
simpa [orderedInsert, h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)
[GOAL]
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if a = b then 1 else 0
[PROOFSTEP]
rw [(L.perm_orderedInsert r b).count_eq, count_cons]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (if a = b then Nat.succ (count a L) else count a L) = count a L + if a = b then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
h✝ : a = b
⊢ Nat.succ (count a L) = count a L + 1
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_zero]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
h✝ : ¬a = b
⊢ count a L = count a L + 0
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_zero]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
b : α
l : List α
⊢ insertionSort r (b :: l) ~ b :: l
[PROOFSTEP]
simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ insertionSort r (a :: b :: l) = a :: b :: l
[PROOFSTEP]
rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]
[GOAL]
case hc
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ r a b
α : Type uu r : α → α → Prop inst✝ : DecidableRel r a b : α l : List α h : Sorted r (a :: b :: l) ⊢ Sorted r (b :: l)
[PROOFSTEP]
exacts [rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
⊢ Sorted r (List.orderedInsert r a (b :: l))
[PROOFSTEP]
by_cases h' : a ≼ b
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))
[PROOFSTEP]
rw [List.orderedInsert, if_pos h', sorted_cons]
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ (∀ (b_1 : α), b_1 ∈ b :: l → r a b_1) ∧ Sorted r (b :: l)
[PROOFSTEP]
exact ⟨forall_mem_cons.2 ⟨h', fun c hc => _root_.trans h' (rel_of_sorted_cons h _ hc)⟩, h⟩
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))
[PROOFSTEP]
suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by simpa [orderedInsert, h', h.of_cons.orderedInsert a l]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
this : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Sorted r (List.orderedInsert r a (b :: l))
[PROOFSTEP]
simpa [orderedInsert, h', h.of_cons.orderedInsert a l]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
[PROOFSTEP]
intro b' bm
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ r b b'
[PROOFSTEP]
cases' show b' = a ∨ b' ∈ l by simpa using (perm_orderedInsert _ _ _).subset bm with be bm
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ b' = a ∨ b' ∈ l
[PROOFSTEP]
simpa using (perm_orderedInsert _ _ _).subset bm
[GOAL]
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
be : b' = a
⊢ r b b'
[PROOFSTEP]
subst b'
[GOAL]
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
bm : a ∈ List.orderedInsert r a l
⊢ r b a
[PROOFSTEP]
exact (total_of r _ _).resolve_left h'
[GOAL]
case neg.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'
[PROOFSTEP]
exact rel_of_sorted_cons h _ bm
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
h : split l = (l₁, l₂)
⊢ split (a :: l) = (a :: l₂, l₁)
[PROOFSTEP]
rw [split, h]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
[PROOFSTEP]
cases' e : split l with l₁ l₂
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
[PROOFSTEP]
injection (split_cons_of_eq _ e).symm.trans h
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ length l₁' ≤ length (a :: l) ∧ length l₂' ≤ length (a :: l)
[PROOFSTEP]
substs l₁' l₂'
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
[PROOFSTEP]
cases' length_split_le e with h₁ h₂
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
h₁ : length l₁ ≤ length l
h₂ : length l₂ ≤ length l
⊢ length (a :: l₂) ≤ length (a :: l) ∧ length l₁ ≤ length (a :: l)
[PROOFSTEP]
exact ⟨Nat.succ_le_succ h₂, Nat.le_succ_of_le h₁⟩
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
h : split (a :: b :: l) = (l₁, l₂)
⊢ length l₁ < length (a :: b :: l) ∧ length l₂ < length (a :: b :: l)
[PROOFSTEP]
cases' e : split l with l₁' l₂'
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
h : split (a :: b :: l) = (l₁, l₂)
l₁' l₂' : List α
e : split l = (l₁', l₂')
⊢ length l₁ < length (a :: b :: l) ∧ length l₂ < length (a :: b :: l)
[PROOFSTEP]
injection (split_cons_of_eq _ (split_cons_of_eq _ e)).symm.trans h
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
h : split (a :: b :: l) = (l₁, l₂)
l₁' l₂' : List α
e : split l = (l₁', l₂')
fst_eq✝ : a :: l₁' = l₁
snd_eq✝ : b :: l₂' = l₂
⊢ length l₁ < length (a :: b :: l) ∧ length l₂ < length (a :: b :: l)
[PROOFSTEP]
substs l₁ l₂
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁' l₂' : List α
e : split l = (l₁', l₂')
h : split (a :: b :: l) = (a :: l₁', b :: l₂')
⊢ length (a :: l₁') < length (a :: b :: l) ∧ length (b :: l₂') < length (a :: b :: l)
[PROOFSTEP]
cases' length_split_le e with h₁ h₂
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁' l₂' : List α
e : split l = (l₁', l₂')
h : split (a :: b :: l) = (a :: l₁', b :: l₂')
h₁ : length l₁' ≤ length l
h₂ : length l₂' ≤ length l
⊢ length (a :: l₁') < length (a :: b :: l) ∧ length (b :: l₂') < length (a :: b :: l)
[PROOFSTEP]
exact ⟨Nat.succ_le_succ (Nat.succ_le_succ h₁), Nat.succ_le_succ (Nat.succ_le_succ h₂)⟩
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
⊢ a :: l ~ l₁' ++ l₂'
[PROOFSTEP]
cases' e : split l with l₁ l₂
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ a :: l ~ l₁' ++ l₂'
[PROOFSTEP]
injection (split_cons_of_eq _ e).symm.trans h
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ a :: l ~ l₁' ++ l₂'
[PROOFSTEP]
substs l₁' l₂'
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ a :: l ~ a :: l₂ ++ l₁
[PROOFSTEP]
exact ((perm_split e).trans perm_append_comm).cons a
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ List α
[PROOFSTEP]
let ls := (split (a :: b :: l))
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
ls : List α × List α := split (a :: b :: l)
⊢ List α
[PROOFSTEP]
have e : split (a :: b :: l) = ⟨ls.1, ls.2⟩ := rfl
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
ls : List α × List α := split (a :: b :: l)
e : split (a :: b :: l) = (ls.fst, ls.snd)
⊢ List α
[PROOFSTEP]
have h := length_split_lt e
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
ls : List α × List α := split (a :: b :: l)
e : split (a :: b :: l) = (ls.fst, ls.snd)
h : length ls.fst < length (a :: b :: l) ∧ length ls.snd < length (a :: b :: l)
⊢ List α
[PROOFSTEP]
have := h.1
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
ls : List α × List α := split (a :: b :: l)
e : split (a :: b :: l) = (ls.fst, ls.snd)
h : length ls.fst < length (a :: b :: l) ∧ length ls.snd < length (a :: b :: l)
this : length ls.fst < length (a :: b :: l)
⊢ List α
[PROOFSTEP]
have := h.2
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
ls : List α × List α := split (a :: b :: l)
e : split (a :: b :: l) = (ls.fst, ls.snd)
h : length ls.fst < length (a :: b :: l) ∧ length ls.snd < length (a :: b :: l)
this✝ : length ls.fst < length (a :: b :: l)
this : length ls.snd < length (a :: b :: l)
⊢ List α
[PROOFSTEP]
exact merge r (mergeSort ls.1) (mergeSort ls.2)
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
h : split (a :: b :: l) = (l₁, l₂)
⊢ mergeSort r (a :: b :: l) = merge r (mergeSort r l₁) (mergeSort r l₂)
[PROOFSTEP]
simp only [mergeSort, h]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
⊢ merge r [] [] ~ [] ++ []
[PROOFSTEP]
simp [merge]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
b : α
l' : List α
⊢ merge r [] (b :: l') ~ [] ++ b :: l'
[PROOFSTEP]
simp [merge]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ merge r (a :: l) [] ~ a :: l ++ []
[PROOFSTEP]
simp [merge]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
[PROOFSTEP]
by_cases h : a ≼ b
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
[PROOFSTEP]
simpa [merge, h] using perm_merge _ _
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
[PROOFSTEP]
suffices b :: merge r (a :: l) l' ~ a :: (l ++ b :: l') by simpa [merge, h]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
this : b :: merge r (a :: l) l' ~ a :: (l ++ b :: l')
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
[PROOFSTEP]
simpa [merge, h]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ b :: merge r (a :: l) l' ~ a :: (l ++ b :: l')
[PROOFSTEP]
exact ((perm_merge _ _).cons _).trans ((swap _ _ _).trans (perm_middle.symm.cons _))
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
⊢ mergeSort r [] ~ []
[PROOFSTEP]
simp [mergeSort]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ mergeSort r [a] ~ [a]
[PROOFSTEP]
simp [mergeSort]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
[PROOFSTEP]
cases' e : split (a :: b :: l) with l₁ l₂
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
[PROOFSTEP]
cases' length_split_lt e with h₁ h₂
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
[PROOFSTEP]
rw [mergeSort_cons_cons r e]
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ merge r (mergeSort r l₁) (mergeSort r l₂) ~ a :: b :: l
[PROOFSTEP]
apply (perm_merge r _ _).trans
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r l₁ ++ mergeSort r l₂ ~ a :: b :: l
[PROOFSTEP]
exact ((perm_mergeSort l₁).append (perm_mergeSort l₂)).trans (perm_split e).symm
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
x✝¹ x✝ : Sorted r []
⊢ Sorted r (List.merge r [] [])
[PROOFSTEP]
simp [List.merge]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
b : α
l' : List α
x✝ : Sorted r []
h₂ : Sorted r (b :: l')
⊢ Sorted r (List.merge r [] (b :: l'))
[PROOFSTEP]
simpa [List.merge] using h₂
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
h₁ : Sorted r (a :: l)
x✝ : Sorted r []
⊢ Sorted r (List.merge r (a :: l) [])
[PROOFSTEP]
simpa [List.merge] using h₁
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
[PROOFSTEP]
by_cases h : a ≼ b
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
[PROOFSTEP]
suffices ∀ (b' : α) (_ : b' ∈ List.merge r l (b :: l')), r a b' by simpa [List.merge, h, h₁.of_cons.merge h₂]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
this : ∀ (b' : α), b' ∈ List.merge r l (b :: l') → r a b'
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
[PROOFSTEP]
simpa [List.merge, h, h₁.of_cons.merge h₂]
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
⊢ ∀ (b' : α), b' ∈ List.merge r l (b :: l') → r a b'
[PROOFSTEP]
intro b' bm
[GOAL]
case pos
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
⊢ r a b'
[PROOFSTEP]
rcases show b' = b ∨ b' ∈ l ∨ b' ∈ l' by simpa [or_left_comm] using (perm_merge _ _ _).subset bm with (be | bl | bl')
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
⊢ b' = b ∨ b' ∈ l ∨ b' ∈ l'
[PROOFSTEP]
simpa [or_left_comm] using (perm_merge _ _ _).subset bm
[GOAL]
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
be : b' = b
⊢ r a b'
[PROOFSTEP]
subst b'
[GOAL]
case pos.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
bm : b ∈ List.merge r l (b :: l')
⊢ r a b
[PROOFSTEP]
assumption
[GOAL]
case pos.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl : b' ∈ l
⊢ r a b'
[PROOFSTEP]
exact rel_of_sorted_cons h₁ _ bl
[GOAL]
case pos.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : r a b
b' : α
bm : b' ∈ List.merge r l (b :: l')
bl' : b' ∈ l'
⊢ r a b'
[PROOFSTEP]
exact _root_.trans h (rel_of_sorted_cons h₂ _ bl')
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
[PROOFSTEP]
suffices ∀ (b' : α) (_ : b' ∈ List.merge r (a :: l) l'), r b b' by simpa [List.merge, h, h₁.merge h₂.of_cons]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
this : ∀ (b' : α), b' ∈ List.merge r (a :: l) l' → r b b'
⊢ Sorted r (List.merge r (a :: l) (b :: l'))
[PROOFSTEP]
simpa [List.merge, h, h₁.merge h₂.of_cons]
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
⊢ ∀ (b' : α), b' ∈ List.merge r (a :: l) l' → r b b'
[PROOFSTEP]
intro b' bm
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
⊢ r b b'
[PROOFSTEP]
have ba : b ≼ a := (total_of r _ _).resolve_left h
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
⊢ r b b'
[PROOFSTEP]
have : b' = a ∨ b' ∈ l ∨ b' ∈ l' := by simpa using (perm_merge _ _ _).subset bm
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
⊢ b' = a ∨ b' ∈ l ∨ b' ∈ l'
[PROOFSTEP]
simpa using (perm_merge _ _ _).subset bm
[GOAL]
case neg
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
this : b' = a ∨ b' ∈ l ∨ b' ∈ l'
⊢ r b b'
[PROOFSTEP]
rcases this with (be | bl | bl')
[GOAL]
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
be : b' = a
⊢ r b b'
[PROOFSTEP]
subst b'
[GOAL]
case neg.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
ba : r b a
bm : a ∈ List.merge r (a :: l) l'
⊢ r b a
[PROOFSTEP]
assumption
[GOAL]
case neg.inr.inl
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl : b' ∈ l
⊢ r b b'
[PROOFSTEP]
exact _root_.trans ba (rel_of_sorted_cons h₁ _ bl)
[GOAL]
case neg.inr.inr
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
l : List α
b : α
l' : List α
h₁ : Sorted r (a :: l)
h₂ : Sorted r (b :: l')
h : ¬r a b
b' : α
bm : b' ∈ List.merge r (a :: l) l'
ba : r b a
bl' : b' ∈ l'
⊢ r b b'
[PROOFSTEP]
exact rel_of_sorted_cons h₂ _ bl'
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
⊢ Sorted r (mergeSort r [])
[PROOFSTEP]
simp [mergeSort]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a : α
⊢ Sorted r (mergeSort r [a])
[PROOFSTEP]
simp [mergeSort]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
⊢ Sorted r (mergeSort r (a :: b :: l))
[PROOFSTEP]
cases' e : split (a :: b :: l) with l₁ l₂
[GOAL]
case mk
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
⊢ Sorted r (mergeSort r (a :: b :: l))
[PROOFSTEP]
cases' length_split_lt e with h₁ h₂
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ Sorted r (mergeSort r (a :: b :: l))
[PROOFSTEP]
rw [mergeSort_cons_cons r e]
[GOAL]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ Sorted r (merge r (mergeSort r l₁) (mergeSort r l₂))
[PROOFSTEP]
exact (sorted_mergeSort l₁).merge (sorted_mergeSort l₂)
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
⊢ mergeSort r [] = []
[PROOFSTEP]
rw [List.mergeSort]
[GOAL]
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ mergeSort r [a] = [a]
[PROOFSTEP]
rw [List.mergeSort]