diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean
index 218f5ff49b..982099329f 100644
--- a/src/Lean/Elab/Tactic/Ext.lean
+++ b/src/Lean/Elab/Tactic/Ext.lean
@@ -85,7 +85,12 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
       if fvars.fvarSet.contains fvar.fvarId! then
         throwError "argument {fvar} is depended upon, which is not supported"
     let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
-    withNewBinderInfos (args |>.extract 0 startIdx |>.map (·.fvarId!, .implicit)) do
+    -- Make everything implicit except for inst implicits
+    let mut newBis := #[]
+    for fvar in args[0:startIdx] do
+      if (← fvar.fvarId!.getBinderInfo) matches .default | .strictImplicit then
+        newBis := newBis.push (fvar.fvarId!, .implicit)
+    withNewBinderInfos newBis do
       mkForallFVars args[:startIdx] <| mkIff ty conj
 
 /--
diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean
index 41929c398a..bfbda098c5 100644
--- a/tests/lean/run/ext.lean
+++ b/tests/lean/run/ext.lean
@@ -128,3 +128,13 @@ theorem MyFun.ext {α β : Type _} (x y : MyFun α β) (h : ∀ a, x.toFun a = y
 info: MyFun.ext_iff.{u_1, u_2} {α : Type u_1} {β : Type u_2} {x y : MyFun α β} : x = y ↔ ∀ (a : α), x.toFun a = y.toFun a
 -/
 #guard_msgs in #check MyFun.ext_iff
+
+
+/-!
+Preserving inst implicits in ext_iff theorem
+-/
+section
+attribute [local ext] Subsingleton.elim
+/-- info: Subsingleton.elim_iff.{u} {α : Sort u} [h : Subsingleton α] {a b : α} : a = b ↔ True -/
+#guard_msgs in #check Subsingleton.elim_iff
+end