chore: more adaptations for lean4#5542 (#17688)

In [lean4#5542](leanprover/lean4#5542) we are deprecating `inductive ... :=`, `structure ... :=`, and `class ... :=` for their `... where` counterparts. Continuation of #17655.

Author: kmill

Diff for: test/Simps.lean

@@ -101,7 +101,7 @@ infix:25 (priority := default+1) " ≃ " => Equiv'
 
 /- Since `prod` and `PProd` are a special case for `@[simps]`, we define a new structure to test
   the basic functionality.-/
-structure MyProd (α β : Type _) := (fst : α) (snd : β)
+structure MyProd (α β : Type _) where (fst : α) (snd : β)
 
 def MyProd.map {α α' β β'} (f : α → α') (g : β → β') (x : MyProd α β) : MyProd α' β' :=
   ⟨f x.1, g x.2⟩

Diff for: test/Traversable.lean

@@ -34,7 +34,7 @@ inductive RecData (α : Type u) : Type u
 
 #guard_msgs (drop info) in #synth LawfulTraversable RecData
 
-unsafe structure MetaStruct (α : Type u) : Type u :=
+unsafe structure MetaStruct (α : Type u) : Type u where
   x : α
   y : ℤ
   z : List α