More cleanup for Sort.lean

Changes

1 changed files (+5/-5)

• Sort.lean
  • @@ -38,7 +38,7 @@ theorem perm : ICan'tBelieveItCanSort.{0} A |>.Perm A := by
    case vc1.step.isTrue => expose_names simp_all only [Multiset.coe_eq_coe] - exact h_5.trans <| .symm <| Vector.perm_iff_toList_perm.mp <| Vector.swap_perm (by grind) (by grind) + exact h_5.trans <| .symm <| Vector.Perm.toList <| Vector.swap_perm (by grind) (by grind) theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by generalize h : ICan'tBelieveItCanSort A = x
  • @@ -46,7 +46,7 @@ theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
    mvcgen <;> expose_names case inv1 => exact ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝ case inv2 => - exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur |>.toArray.Pairwise (· ≤ ·)) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by + exact ⇓⟨xs, A'⟩ => ⌜(A'.take cur).toArray.Pairwise (· ≤ ·) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by have : xs.prefix.length + xs.suffix.length = N := by simp [← List.length_append, xs.property] grind ) ≤ A'[cur]'(by grind)⌝
  • @@ -69,8 +69,8 @@ theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
    case vc5.a.pre => grind case vc6.a.post.success => simp_all - rwa [show r.toArray = r.toArray.extract 0 N by grind] + exact (show r.toArray = r.toArray.extract 0 N by grind) ▸ h_1 - theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A |>.Perm A) - ∧ (ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·)) := + theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A + ∧ (ICan'tBelieveItCanSort.{0} A).Pairwise (· ≤ ·) := ⟨perm A, sorted A⟩