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