diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index 5cb6c8e110..5c8cfc7b78 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -145,7 +145,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
       congrTheorems := (← getSimpCongrTheorems)
       config        := Simp.neutralConfig
     }
-  let tgt ← mvarId.getType
+  let tgt ← instantiateMVars (← mvarId.getType)
   let res ← Simp.main tgt simpCtx (methods := { post })
   let newGoal ← applySimpResultToTarget mvarId tgt res
   newGoal.refl
diff --git a/tests/lean/run/1202.lean b/tests/lean/run/1202.lean
new file mode 100644
index 0000000000..7dc31d54f5
--- /dev/null
+++ b/tests/lean/run/1202.lean
@@ -0,0 +1,16 @@
+opaque f : Bool → Bool → Bool
+axiom f_comm (a b : Bool) : f a b = f b a
+axiom f_assoc (a b c : Bool) : f (f a b) c = f a (f b c)
+instance : Lean.IsCommutative f := ⟨f_comm⟩
+instance : Lean.IsAssociative f := ⟨f_assoc⟩
+
+example (a b c : Bool) : f (f a b) c = f (f a c) b :=
+  by ac_rfl -- good
+
+example (a b c : Bool) : (f (f a b) c = f (f a c) b) ∧ true :=
+  And.intro (by ac_rfl) rfl -- good
+
+example (a b c : Bool) : (f (f a b) c = f (f a c) b) ∧ true := by
+  apply And.intro
+  . ac_rfl
+  . rfl