test: add example from issue

closes #4534

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -123,7 +123,14 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           return none
         pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
-      if e == rhs then
+      /-
+      We used to use `e == rhs` in the following test.
+      However, it include unnecessary proof steps when `e` and `rhs`
+      are equal after metavariables are instantiated.
+      We are hoping the following `instantiateMVars` should not be too expensive since
+      we seldom have assigned metavariables in goals.
+      -/
+      if (← instantiateMVars e) == rhs then
         return none
       if thm.perm then
         /-

tests/lean/run/4534.lean

@@ -0,0 +1,17 @@
+universe u
+
+class MyClass (α : Type u) extends LE α where
+  sup : α → α → α
+  le_refl : ∀ a : α, a ≤ a
+  sup_of_le_left : ∀ a b : α, b ≤ a → sup a b = a
+
+instance : MyClass Prop where
+  le_refl _ := id
+  sup_of_le_left _ _ h := propext ⟨Or.rec id h, Or.inl⟩
+
+/--
+info: Try this: simp only [MyClass.le_refl, MyClass.sup_of_le_left]
+-/
+#guard_msgs in
+example : MyClass.sup False False = False := by
+  simp? [MyClass.sup_of_le_left, MyClass.le_refl]