diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3fe086dd9c..c1abb89cb5 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -793,10 +793,10 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
     | _            => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
 
 /--
-  If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal.
-  If they are not, then try coercions.
+If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
 
-  Argument `f?` is used only for generating error messages. -/
+Argument `f?` is used only for generating error messages when inserting coercions fails.
+-/
 def ensureHasType (expectedType? : Option Expr) (e : Expr)
     (errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
   let some expectedType := expectedType? | return e
@@ -1432,9 +1432,22 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
   withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
 
+/--
+Similar to `Lean.Elab.Term.elabTerm`, but ensures that the type of the elaborated term is `expectedType?`
+by inserting coercions if necessary.
+
+If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
+Otherwise, it throws the error.
+-/
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
-  withRef stx <| ensureHasType expectedType? e errorMsgHeader?
+  try
+    withRef stx <| ensureHasType expectedType? e errorMsgHeader?
+  catch ex =>
+    if (← read).errToSorry && ex matches .error .. then
+      exceptionToSorry ex expectedType?
+    else
+      throw ex
 
 /-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`. -/
 def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
diff --git a/tests/lean/issue2260.lean.expected.out b/tests/lean/issue2260.lean.expected.out
index 66e493b51c..fdcd0e62cb 100644
--- a/tests/lean/issue2260.lean.expected.out
+++ b/tests/lean/issue2260.lean.expected.out
@@ -13,3 +13,10 @@ The termination argument has type
   DNat i : Type
 but is expected to have type
   Nat : Type
+issue2260.lean:26:15-26:21: error: failed to prove termination, possible solutions:
+  - Use `have`-expressions to prove the remaining goals
+  - Use `termination_by` to specify a different well-founded relation
+  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
+n✝ : Nat
+n : DNat n✝
+⊢ sorryAx Nat true < 1 + n✝ + sizeOf n
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index 11c697d680..c84c427000 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -14,6 +14,12 @@ has type
   true = true : Prop
 but is expected to have type
   true = false : Prop
+mulcommErrorMessage.lean:12:22-12:25: error: type mismatch
+  rfl
+has type
+  false = false : Prop
+but is expected to have type
+  false = true : Prop
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
   fun a b => ?m a b
 has type
diff --git a/tests/lean/run/haveTactic.lean b/tests/lean/run/haveTactic.lean
new file mode 100644
index 0000000000..54edb02fb6
--- /dev/null
+++ b/tests/lean/run/haveTactic.lean
@@ -0,0 +1,24 @@
+/-!
+# Tests for the `have` tactic.
+-/
+
+/-!
+If the body of a `have` fails to elaborate, the tactic completes with a `sorry` for the proof.
+-/
+/--
+error: type mismatch
+  False.elim
+has type
+  False → ?m.6 : Sort ?u.5
+but is expected to have type
+  True : Prop
+---
+info: h : True
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  have h : True :=
+    False.elim
+  trace_state
+  assumption
diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean
index f6cc3037f4..143da10cc0 100644
--- a/tests/lean/struct1.lean
+++ b/tests/lean/struct1.lean
@@ -31,13 +31,13 @@ structure S :=
 structure S extends A Nat :=
 (x : Nat) -- error
 
-structure S extends A Nat :=
+structure S' extends A Nat :=
 (x := true) -- error type mismatch
 
 structure S extends A Nat :=
 (x : Bool := true) -- error omit type
 
-structure S :=
+structure S'' :=
 (x : Nat := true) -- error type mismatch
 
 private structure S :=