diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 459f5f35ff..ab0fa565b2 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -96,9 +96,28 @@ def apply (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) :=
     result.forM headBetaMVarType
     return result
 
-def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := do
-  saturate mvarId fun mvarId =>
-    observing? <| apply mvarId (mkConst ``And.intro)
+partial def splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `splitAnd
+    let type ← getMVarType' mvarId
+    if !type.isAppOfArity ``And 2 then
+      return [mvarId]
+    else
+      let tag ← getMVarTag mvarId
+      let rec go (type : Expr) : StateRefT (Array MVarId) MetaM Expr := do
+        let type ← whnf type
+        if type.isAppOfArity ``And 2 then
+          let p₁ := type.appFn!.appArg!
+          let p₂ := type.appArg!
+          return mkApp4 (mkConst ``And.intro) p₁ p₂ (← go p₁) (← go p₂)
+        else
+          let idx := (← get).size + 1
+          let mvar ← mkFreshExprSyntheticOpaqueMVar type (tag ++ (`h).appendIndexAfter idx)
+          modify fun s => s.push mvar.mvarId!
+          return mvar
+      let (val, s) ← go type |>.run #[]
+      assignExprMVar mvarId val
+      return s.toList
 
 def applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Unit :=
   withMVarContext mvarId do
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 1329187552..65bfdd689f 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -14,7 +14,7 @@ a : α
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-    [.] `Fam2 : some Sort.{?_uniq.288} @ ⟨7, 21⟩-⟨7, 25⟩
+    [.] `Fam2 : some Sort.{?_uniq.272} @ ⟨7, 21⟩-⟨7, 25⟩
     Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
     α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
       α : Type @ ⟨7, 26⟩-⟨7, 27⟩
@@ -45,7 +45,7 @@ a : α
     ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
       ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
     Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
-      [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.618]) ([mdata _inaccessible:1 ?_uniq.619]) @ ⟨9, 4⟩-⟨9, 12⟩
+      [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.602]) ([mdata _inaccessible:1 ?_uniq.603]) @ ⟨9, 4⟩-⟨9, 12⟩
       @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
       ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
         ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
@@ -61,7 +61,7 @@ a : α
     Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
       Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
     Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp
-      [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.650]) ([mdata _inaccessible:1 ?_uniq.651]) @ ⟨10, 4⟩-⟨10, 12⟩
+      [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.634]) ([mdata _inaccessible:1 ?_uniq.635]) @ ⟨10, 4⟩-⟨10, 12⟩
       Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
       n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent
         n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 3311c7c767..fd2709f924 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -1,6 +1,6 @@
 [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration
   Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.417} @ ⟨13, 11⟩-⟨13, 14⟩
+    [.] `Nat : some Sort.{?_uniq.385} @ ⟨13, 11⟩-⟨13, 14⟩
     Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
   x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
   Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1»
@@ -11,10 +11,10 @@
       Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp
         Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩†
         Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent
-          [.] `Nat : some Type.{?_uniq.421} @ ⟨13, 18⟩-⟨13, 21⟩
+          [.] `Nat : some Type.{?_uniq.389} @ ⟨13, 18⟩-⟨13, 21⟩
           Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
         Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
-          [.] `Nat : some Type.{?_uniq.420} @ ⟨13, 24⟩-⟨13, 27⟩
+          [.] `Nat : some Type.{?_uniq.388} @ ⟨13, 24⟩-⟨13, 27⟩
           Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
   x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
   let y := (x, x);
@@ -41,16 +41,16 @@
 [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration
   ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
     Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.450} @ ⟨17, 15⟩-⟨17, 18⟩
+      [.] `Nat : some Sort.{?_uniq.418} @ ⟨17, 15⟩-⟨17, 18⟩
       Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
     x (isBinder := true) : Nat @ ⟨17, 9⟩-⟨17, 10⟩
     Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.452} @ ⟨17, 15⟩-⟨17, 18⟩
+      [.] `Nat : some Sort.{?_uniq.420} @ ⟨17, 15⟩-⟨17, 18⟩
       Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
     y (isBinder := true) : Nat @ ⟨17, 11⟩-⟨17, 12⟩
     Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
       Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent
-        [.] `Bool : some Sort.{?_uniq.455} @ ⟨17, 27⟩-⟨17, 31⟩
+        [.] `Bool : some Sort.{?_uniq.423} @ ⟨17, 27⟩-⟨17, 31⟩
         Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
       b (isBinder := true) : Bool @ ⟨17, 23⟩-⟨17, 24⟩
       x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
@@ -112,20 +112,20 @@
 [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration
   Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
     Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.574} @ ⟨21, 16⟩-⟨21, 19⟩
+      [.] `Nat : some Sort.{?_uniq.542} @ ⟨21, 16⟩-⟨21, 19⟩
       Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
     x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩
     Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.576} @ ⟨21, 16⟩-⟨21, 19⟩
+      [.] `Nat : some Sort.{?_uniq.544} @ ⟨21, 16⟩-⟨21, 19⟩
       Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
     y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩
     Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
       Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent
-        [.] `Bool : some Sort.{?_uniq.579} @ ⟨21, 28⟩-⟨21, 32⟩
+        [.] `Bool : some Sort.{?_uniq.547} @ ⟨21, 28⟩-⟨21, 32⟩
         Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
       b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩
       Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
-        [.] `Nat : some Sort.{?_uniq.581} @ ⟨21, 36⟩-⟨21, 39⟩
+        [.] `Nat : some Sort.{?_uniq.549} @ ⟨21, 36⟩-⟨21, 39⟩
         Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
   fun x y b =>
     let x := (x + y, x - y);
@@ -238,10 +238,10 @@
       Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
         Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
         Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
-          [.] `Nat : some Type.{?_uniq.795} @ ⟨27, 12⟩-⟨27, 15⟩
+          [.] `Nat : some Type.{?_uniq.763} @ ⟨27, 12⟩-⟨27, 15⟩
           Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
         Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
-          [.] `Array : some Type.{?_uniq.794} @ ⟨27, 18⟩-⟨27, 23⟩
+          [.] `Array : some Type.{?_uniq.762} @ ⟨27, 18⟩-⟨27, 23⟩
           Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
           Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
             Macro expansion
@@ -249,17 +249,17 @@
             ===>
             Array Nat
               Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
-                [.] `Array : some Type.{?_uniq.796} @ ⟨27, 25⟩-⟨27, 30⟩
+                [.] `Array : some Type.{?_uniq.764} @ ⟨27, 25⟩-⟨27, 30⟩
                 Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
                 Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
-                  [.] `Nat : some Type.{?_uniq.797} @ ⟨27, 31⟩-⟨27, 34⟩
+                  [.] `Nat : some Type.{?_uniq.765} @ ⟨27, 31⟩-⟨27, 34⟩
                   Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
   s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
   Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
-    [.] `Array : some Sort.{?_uniq.799} @ ⟨27, 39⟩-⟨27, 44⟩
+    [.] `Array : some Sort.{?_uniq.767} @ ⟨27, 39⟩-⟨27, 44⟩
     Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
     Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Type.{?_uniq.800} @ ⟨27, 45⟩-⟨27, 48⟩
+      [.] `Nat : some Type.{?_uniq.768} @ ⟨27, 45⟩-⟨27, 48⟩
       Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
   s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
   Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
@@ -275,11 +275,11 @@
   f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
 [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
   B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.842} @ ⟨30, 14⟩-⟨30, 15⟩
+    [.] `B : some Sort.{?_uniq.810} @ ⟨30, 14⟩-⟨30, 15⟩
     B : Type @ ⟨30, 14⟩-⟨30, 15⟩
   arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
   Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.844} @ ⟨30, 19⟩-⟨30, 22⟩
+    [.] `Nat : some Sort.{?_uniq.812} @ ⟨30, 19⟩-⟨30, 22⟩
     Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
   arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
   A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
@@ -294,11 +294,11 @@
   f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩
 [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
   Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.865} @ ⟨33, 12⟩-⟨33, 15⟩
+    [.] `Nat : some Sort.{?_uniq.833} @ ⟨33, 12⟩-⟨33, 15⟩
     Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
   x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
   B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.867} @ ⟨33, 19⟩-⟨33, 20⟩
+    [.] `B : some Sort.{?_uniq.835} @ ⟨33, 19⟩-⟨33, 20⟩
     B : Type @ ⟨33, 19⟩-⟨33, 20⟩
   x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
   { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
@@ -338,73 +338,73 @@ infoTree.lean:44:0: error: expected stx
   [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
 [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
   Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.889} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.857} @ ⟨45, 14⟩-⟨45, 17⟩
     Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.890 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.858 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
   Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
-    [.] `Nat : some Sort.{?_uniq.891} @ ⟨45, 14⟩-⟨45, 17⟩
+    [.] `Nat : some Sort.{?_uniq.859} @ ⟨45, 14⟩-⟨45, 17⟩
     Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
-  _uniq.892 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  Eq.{1} Nat _uniq.890 _uniq.890 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+  _uniq.860 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
     Macro expansion
     («term_=_» `x "=" `x)
     ===>
     (Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x)
-      Eq.{1} Nat _uniq.890 _uniq.890 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
-        _uniq.890 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
-          _uniq.890 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
-        _uniq.890 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
-          _uniq.890 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
-  _uniq.899 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
-  _uniq.900 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
-  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.899 _uniq.900]) f6.f7 : Eq.{1} Nat _uniq.899 _uniq.899 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
+      Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
+        _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
+          _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
+        _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
+          _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
+  _uniq.867 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
+  _uniq.868 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
+  (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.867 _uniq.868]) f6.f7 : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
     Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.901} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.869} @ ⟨46, 20⟩-⟨46, 23⟩
       Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.902 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.870 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
     Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
-      [.] `Nat : some Sort.{?_uniq.903} @ ⟨46, 20⟩-⟨46, 23⟩
+      [.] `Nat : some Sort.{?_uniq.871} @ ⟨46, 20⟩-⟨46, 23⟩
       Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
-    _uniq.904 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.{1} Nat _uniq.902 _uniq.902 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
+    _uniq.872 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
       Macro expansion
       («term_=_» `x "=" `x)
       ===>
       (Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x)
-        Eq.{1} Nat _uniq.902 _uniq.902 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
-          _uniq.902 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
-            _uniq.902 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
-          _uniq.902 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
-            _uniq.902 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
-    _uniq.909 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
-    _uniq.912 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
-    _uniq.913 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
-    Eq.refl.{1} Nat _uniq.912 : Eq.{1} Nat _uniq.912 _uniq.912 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
-      [.] `Eq.refl : some Eq.{?_uniq.906} Nat _uniq.912 _uniq.912 @ ⟨46, 36⟩-⟨46, 43⟩
+        Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
+          _uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
+            _uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
+          _uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
+            _uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
+    _uniq.877 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
+    _uniq.880 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
+    _uniq.881 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
+    Eq.refl.{1} Nat _uniq.880 : Eq.{1} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
+      [.] `Eq.refl : some Eq.{?_uniq.874} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 43⟩
       Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
-      _uniq.912 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.912 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
-    [mdata _recApp: _uniq.909 _uniq.899 _uniq.900] : Eq.{1} Nat _uniq.899 _uniq.899 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
-      _uniq.909 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
-      _uniq.899 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.899 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
-      _uniq.900 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
-        _uniq.900 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
+      _uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
+    [mdata _recApp: _uniq.877 _uniq.867 _uniq.868] : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
+      _uniq.877 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
+      _uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
+      _uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
+        _uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
   f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
   f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
 [Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
   B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.937} @ ⟨50, 12⟩-⟨50, 13⟩
+    [.] `B : some Sort.{?_uniq.905} @ ⟨50, 12⟩-⟨50, 13⟩
     B : Type @ ⟨50, 12⟩-⟨50, 13⟩
-  _uniq.938 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  _uniq.906 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
   B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
-    [.] `B : some Sort.{?_uniq.939} @ ⟨50, 17⟩-⟨50, 18⟩
+    [.] `B : some Sort.{?_uniq.907} @ ⟨50, 17⟩-⟨50, 18⟩
     B : Type @ ⟨50, 17⟩-⟨50, 18⟩
-  _uniq.942 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
-  B.mk (B.pair _uniq.942) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
-    B.pair _uniq.942 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
-      _uniq.942 : B @ ⟨50, 24⟩-⟨50, 25⟩
-      [.] _uniq.942 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
+  _uniq.910 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
+  B.mk (B.pair _uniq.910) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
+    B.pair _uniq.910 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
+      _uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩
+      [.] _uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
       B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
-    pair : Prod.{0 0} A A := B.pair _uniq.942 @ ⟨50, 22⟩†-⟨50, 32⟩
+    pair : Prod.{0 0} A A := B.pair _uniq.910 @ ⟨50, 22⟩†-⟨50, 32⟩
   f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index 9ded66f6b2..ac1158f85d 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,18 +1,3 @@
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
 jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
 context:
@@ -43,41 +28,6 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
-jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.arrow G T EG getCtx
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx
-        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
-    (TAlgebra
-      (@TySyntaxLayer.nat G T EG getCtx
-        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
-    (@EGrfl
-      (getCtx
-        (TAlgebra
-          (@TySyntaxLayer.nat G T EG getCtx
-            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
-x✝ : G
-⊢ G
 jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
   @EGrfl
     (getCtx
@@ -131,3 +81,53 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
 x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
 x✝ : G
 ⊢ G
+jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.arrow G T EG getCtx
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx
+        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
+    (TAlgebra
+      (@TySyntaxLayer.nat G T EG getCtx
+        (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
+    (@EGrfl
+      (getCtx
+        (TAlgebra
+          (@TySyntaxLayer.nat G T EG getCtx
+            (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))))
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
+x✝ : G
+⊢ G
diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
index 21443d2f22..29ef951454 100644
--- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out
+++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out
@@ -1,11 +1,3 @@
-syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
-context:
-α β : Type
-a✝ : α
-x : Fam2 α β
-a : Nat
-n : Nat
-⊢ Nat
 syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
@@ -14,6 +6,14 @@ x : Fam2 α✝ β
 α : Type
 a : α
 ⊢ α
+syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
+context:
+α β : Type
+a✝ : α
+x : Fam2 α β
+a : Nat
+n : Nat
+⊢ Nat
 syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type