choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
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 ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
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 ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)