simp vs rw behavior with lemmas supplied by instances

Stream: lean4

[Yakov Pechersky]

Consider:

def liftOrGet (f : α → α → α) : Option α → Option α → Option α
  | none, none => none
  | some a, none => some a
  | none, some b => some b
  | some a, some b => some (f a b)

class IsCommutative (α : Type u) (op : α → α → α) : Prop where
  comm : ∀ a b, op a b = op b a

instance (f : α → α → α) [h : IsCommutative α f] :
    IsCommutative (Option α) (liftOrGet f) :=
  ⟨fun a b => by cases a <;> cases b <;> simp [liftOrGet, h.comm]⟩ -- doesn't work

instance (f : α → α → α) [h : IsCommutative α f] :
    IsCommutative (Option α) (liftOrGet f) :=
  ⟨fun a b => by cases a <;> cases b <;> simp [liftOrGet] <;> rw [h.comm]⟩ -- works

[Yakov Pechersky]

The first proof does work in lean3 AFAIU

[Kevin Buzzard]

Lean 3's simp was clever with comm lemmas. What happens here? Does it loop?

[Yakov Pechersky]

The h.comm doesn't ever fire. The same would happen if I was showcasing IsAssociative