A commutative simple ring is a principal ideal domain

Indeed, it is a field.

instance instIsSimpleOrderIdeal {R : Type u_1} [CommRing R] [IsSimpleRing R] : IsSimpleOrder (Ideal R)

instance IsPrincipalIdealRing.of_isSimpleRing {R : Type u_1} [CommRing R] [IsSimpleRing R] : IsPrincipalIdealRing R

instance IsDomain.of_isSimpleRing {R : Type u_1} [CommRing R] [IsSimpleRing R] : IsDomain R