Yay even shorter proof

Changes

1 changed files (+2/-8)

• Sort.lean
  • @@ -34,11 +34,5 @@ return
    set_option maxHeartbeats 1000000 in prove_correct ICan'tBelieveItCanSort by loom_solve - intro k h₁ h₂ - by_cases h : k = j - · have : ((A_1.set! i A_1[j]!).set! j A_1[i]!)[k - 1]! = A_1[k - 1]! := by grind - rw [this] - have : ((A_1.set! i A_1[j]!).set! j A_1[i]!)[k]! = A_1[i]! := by grind - rw [this] - exact invariant_5 (k - 1) (by grind) (by grind) - · grind + intro k _ _ + by_cases k = j <;> grind