no goals
ι : Type u_3
R : Type u_2
S : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsDomain R
inst✝⁹ : IsPrincipalIdealRing R
inst✝⁸ : IsDomain S
inst✝⁷ : Fintype ι
F : Type u_1
inst✝⁶ : CommRing F
inst✝⁵ : Algebra F R
inst✝⁴ : Algebra F S
inst✝³ : IsScalarTower F R S
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
inst✝² : Nontrivial F
inst✝¹ : ∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})
inst✝ : ∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})
⊢ FiniteDimensional.finrank F (S ⧸ I) = ∑ i : ι, FiniteDimensional.finrank F (R ⧸ span {smithCoeffs b I hI i})
rw [LinearEquiv.finrank_eq <| Ideal.quotientEquivDirectSum F b hI,
  FiniteDimensional.finrank_directSum]