structure A
structure B

theorem stuff : A = B := sorry

example : B := by
  set_option tactic.simp.trace true in
  simp [← stuff] -- Try this: simp only [stuff] // should be: simp only [← stuff]
  exact A.mk