Simpler proof

Changes

1 changed files (+3/-8)

• Sort.lean
  • @@ -36,14 +36,9 @@ prove_correct ICan'tBelieveItCanSort by
    loom_solve intro k h₁ h₂ by_cases h : k = j - · simp [h] - have : j ≠ k - 1 := by grind - have : i ≠ k - 1 := by grind - have : ((A_1.set! i A_1[j]!).set! j A_1[i]!)[j - 1]! = A_1[j - 1]! := by grind - simp at this + · 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]!)[j]! = A_1[i]! := by grind - simp at 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 (j - 1) (by grind) (by grind) + exact invariant_5 (k - 1) (by grind) (by grind) · grind