feat: add [ext] attribute to Array.ext (#4970)

This fixes a minor papercut.

Author: david-christiansen

src/Init/Ext.lean

@@ -78,7 +78,7 @@ end Elab.Tactic.Ext
 end Lean
 
 attribute [ext] Prod PProd Sigma PSigma
-attribute [ext] funext propext Subtype.eq
+attribute [ext] funext propext Subtype.eq Array.ext
 
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl

tests/lean/run/ext.lean

@@ -82,6 +82,11 @@ example (f : ℕ × (ℕ → ℕ)) : f = f := by
 example (f : Empty → Empty) : f = f := by
   ext ⟨⟩
 
+example (xs : Array α) : xs.map id = xs := by
+  ext
+  . simp
+  . simp
+
 @[ext (iff := false)] theorem ext_intros {n m : Nat} (w : ∀ n m : Nat, n = m) : n = m := by apply w
 
 #guard_msgs (drop warning) in