conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ Fintype.card (Module.Free.ChooseBasisIndex R S)