feat: add LawfulBEq instance for Vector

[mehbark]

The eq_of_beq proof is a bit hairy, and I couldn't find a proof that didn't use Vector.ext, so I moved the instance to be with the other Vector lemmas. All review is greatly appreciated.

[mehbark]

awaiting-review

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1104 has successfully built against this PR. (2025-01-30 00:32:50) View Log
• 🟡 Mathlib branch batteries-pr-testing-1104 build against this PR was cancelled. (2025-01-30 01:57:08) View Log
• 💥 Mathlib branch batteries-pr-testing-1104 build failed against this PR. (2025-01-30 02:33:14) View Log
• 🟡 Mathlib branch batteries-pr-testing-1104 build against this PR was cancelled. (2025-01-30 03:17:41) View Log
• 🟡 Mathlib branch batteries-pr-testing-1104 build against this PR was cancelled. (2025-01-30 03:37:32) View Log
• 🟡 Mathlib branch batteries-pr-testing-1104 build against this PR was cancelled. (2025-01-30 03:40:50) View Log
• 💥 Mathlib branch batteries-pr-testing-1104 build failed against this PR. (2025-01-30 04:21:39) View Log
• ✅ Mathlib branch batteries-pr-testing-1104 has successfully built against this PR. (2025-01-30 10:28:30) View Log
• ✅ Mathlib branch batteries-pr-testing-1104 has successfully built against this PR. (2025-01-31 02:32:08) View Log

[mehbark]

awaiting-review

[mehbark]

If simp_all is undesirable, I can remove it.

[fgdorais]

Minor

[fgdorais]

We need to wait until Mathlib builds but otherwise all good. The Mathlib issue appears to be elsewhere, so no need to worry.

[fgdorais]

I just noticed that Array.rel_of_isEqv is remarkably inconvenient to use. It should be a pair of lemmas:

theorem size_eq_size_of_isEqv {v₁ v₂ : Array α} : v₁.isEqv v₂ r → v₁.size = v₂.size := sorry

theorem getElem_rel_getElem_of_isEqv {v₁ v₂ : Array α} {h₁ : i < v₁.size} {h₂ : i < v₂.size} : v₁.isEqv v₂ r → r v₁[i] v₂[i] := sorry

What do you think @kim-em ?

[fgdorais]

If you want to avoid Vector.ext consider adding the missing lemma:

theorem Vector.isEqv_eq_toArray_isEqv_toArray (v₁ v₂ : Vector α n) : v₁.isEqv v₂ r = v₁.toArray.isEqv v₂.toArray r :=
  match v₁, v₂ with | ⟨_,_⟩, ⟨_,_⟩ => mk_isEqv_mk ..

And the companion for ==.

[mehbark]

awaiting-author

[mehbark]

I'm much more happy with the size of the proof now; thank you!

[mehbark]

awaiting-review

[fgdorais]

Thank you!