From 30a52b794a39256361050c52fe0e41bbff91bc8d Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 9 Aug 2024 14:40:39 +0200
Subject: [PATCH] feat: add [ext] attribute to Array.ext (#4970)

This fixes a minor papercut.
---
 src/Init/Ext.lean       | 2 +-
 tests/lean/run/ext.lean | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean
index 5e084022f4..ad860a15e7 100644
--- a/src/Init/Ext.lean
+++ b/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
diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean
index 5d423f332a..36906a67a3 100644
--- a/tests/lean/run/ext.lean
+++ b/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