no goals
ι : Type ?u.81246
α : Type u_1
β : Type ?u.81252
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
inst✝ : IsRefl α r
⊢ PartiallyWellOrderedOn (insert a s) r ↔ PartiallyWellOrderedOn s r
simp only [← singleton_union, partiallyWellOrderedOn_union,
  partiallyWellOrderedOn_singleton, true_and_iff]