/-- error: No goals to be solved -/
#guard_msgs in
example : 3 = 3 := by
  rfl
  rfl