∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Algebra R S] [Finite ι] (b : Module.Basis ι R S) (I : Ideal S),
  I ≠ ⊥ → Module.finrank R ↥(Submodule.restrictScalars R I) = Module.finrank R S