diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 4c49d4c792..ce07129b45 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -541,7 +541,7 @@ mutual
   /--
     Process a `fType` of the form `(x : A) → B x`.
     This method assume `fType` is a function type -/
-  private partial def processExplictArg (argName : Name) : M Expr := do
+  private partial def processExplicitArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
       if (← anyNamedArgDependsOnCurrent) then
@@ -586,6 +586,16 @@ mutual
         | Except.ok tacticSyntax =>
           -- TODO(Leo): does this work correctly for tactic sequences?
           let tacticBlock ← `(by $(⟨tacticSyntax⟩))
+          /-
+          We insert position information from the current ref into `stx` everywhere, simulating this being
+          a tactic script inserted by the user, which ensures error messages and logging will always be attributed
+          to this application rather than sometimes being placed at position (1,0) in the file.
+          Placing position information on `by` syntax alone is not sufficient since incrementality
+          (in particular, `Lean.Elab.Term.withReuseContext`) controls the ref to avoid leakage of outside data.
+          Note that `tacticSyntax` contains no position information itself, since it is erased by `Lean.Elab.Term.quoteAutoTactic`.
+          -/
+          let info := (← getRef).getHeadInfo
+          let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
           let argNew := Arg.stx tacticBlock
           propagateExpectedType argNew
           elabAndAddNewArg argName argNew
@@ -615,7 +625,7 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      processExplictArg argName
+      processExplicitArg argName
     else
       addImplicitArg argName
 
@@ -624,7 +634,7 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processStrictImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      processExplictArg argName
+      processExplicitArg argName
     else if (← hasArgsToProcess) then
       addImplicitArg argName
     else
@@ -643,7 +653,7 @@ mutual
         addNewArg argName arg
         main
       else
-        processExplictArg argName
+        processExplicitArg argName
     else
       let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
       addInstMVar arg.mvarId!
@@ -668,7 +678,7 @@ mutual
         | .implicit       => processImplicitArg binderName
         | .instImplicit   => processInstImplicitArg binderName
         | .strictImplicit => processStrictImplicitArg binderName
-        | _               => processExplictArg binderName
+        | _               => processExplicitArg binderName
     else if (← hasArgsToProcess) then
       synthesizePendingAndNormalizeFunType
       main
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 53c8815071..cc4706f234 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -677,6 +677,10 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
             | .error err       => throwError err
             | .ok tacticSyntax =>
               let stx ← `(by $tacticSyntax)
+              -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`.
+              -- We add info to get reliable positions for messages from evaluating the tactic script.
+              let info := field.ref.getHeadInfo
+              let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field
           | _ =>
             if bi == .instImplicit then
diff --git a/tests/lean/interactive/4880.lean b/tests/lean/interactive/4880.lean
new file mode 100644
index 0000000000..6a463b4cf9
--- /dev/null
+++ b/tests/lean/interactive/4880.lean
@@ -0,0 +1,36 @@
+/-!
+# Ensure autoparam errors are placed at elaboration position
+
+Before, errors were placed at the beginning of the file.
+-/
+
+
+/-!
+Testing `infer_instance`, which defers a typeclass problem beyond the tactic script execution.
+-/
+class A
+
+-- For structure instance elaboration ...
+structure B where
+  h1 : A := by infer_instance
+
+example : B where
+          --^ collectDiagnostics
+
+-- ... and for app elaboration.
+def baz (_h1 : A := by infer_instance) : Nat := 1
+
+example : Nat := baz
+               --^ collectDiagnostics
+
+
+/-!
+Testing a tactic that immediately throws an error, but incrementality resets the ref
+from the syntax for the tactic (which would be a `.missing` position for autoparams).
+-/
+
+structure B' where
+  h1 : A := by done
+
+example : B' where
+           --^ collectDiagnostics
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
new file mode 100644
index 0000000000..bea1021183
--- /dev/null
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -0,0 +1,32 @@
+{"version": 1,
+ "uri": "file:///4880.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}},
+   "message":
+   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 16, "character": 12},
+    "end": {"line": 16, "character": 17}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 22, "character": 17},
+    "end": {"line": 22, "character": 20}},
+   "message":
+   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 22, "character": 17},
+    "end": {"line": 22, "character": 20}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 34, "character": 13},
+    "end": {"line": 34, "character": 18}},
+   "message": "unsolved goals\n⊢ A",
+   "fullRange":
+   {"start": {"line": 34, "character": 13},
+    "end": {"line": 34, "character": 18}}}]}