-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal R
q : Ideal S
inst_4 : q.IsPrime
inst_5 : p.IsPrime
inst_6 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_7 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_8 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
φ₁ : AlgHom.{u_1, u_1, u_2} R p.ResidueField
  (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)) :=
  Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)
    (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  TensorProduct.lift φ₁
    (IsScalarTower.toAlgHom R S
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p)))
    ⋯
φ₃ : Localization.AtPrime (R := p.Fiber S) Q →ₐ[R]
  HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :=
  IsLocalization.liftAlgHom (R := p.Fiber S) (M := Q.primeCompl) (f := φ₂) ⋯
this :
  Function.Surjective (α := Localization.AtPrime (R := p.Fiber S) Q) (β :=
    HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
inst : QuasiFiniteAt R (S := p.Fiber S) Q
⊢ QuasiFinite.{u_1, u_2} R
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
        (Ideal.under R q)))
have obtain : ∀ [inst : Ideal.IsPrime (Ideal.under R q)] [inst_9 : q.LiesOver (Ideal.under R q)]
  (Q : Ideal (Ideal.Fiber (Ideal.under R q) S)) [inst_10 : Q.IsPrime]
  (hQ :
    Ideal.comap (F := S →+* TensorProduct R (Ideal.ResidueField (Ideal.under R q)) S)
        (AlgHom.toRingHom TensorProduct.includeRight) Q =
      q)
  [QuasiFiniteAt (Ideal.ResidueField (Ideal.under R q)) (S := Ideal.Fiber (Ideal.under R q) S) Q],
  let this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R q)) (Localization.AtPrime q) :=
    Localization.AtPrime.algebraOfLiesOver (Ideal.under R q) q;
  let φ₁ :
    AlgHom.{u_1, u_1, u_2} R (Ideal.ResidueField (Ideal.under R q))
      (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))) :=
    Ideal.quotientMapₐ (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))
      (IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under R q)) Sq) sorry;
  let φ₂ :
    Ideal.Fiber (Ideal.under R q) S →ₐ[R]
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)) :=
    TensorProduct.lift φ₁
      (IsScalarTower.toAlgHom R S
        (HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q))))
      sorry;
  let φ₃ :
    Localization.AtPrime (R := Ideal.Fiber (Ideal.under R q) S) Q →ₐ[R]
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)) :=
    IsLocalization.liftAlgHom (R := Ideal.Fiber (Ideal.under R q) S) (M := Q.primeCompl) (f := φ₂) sorry;
  ∀
    (this :
      Function.Surjective (α := Localization.AtPrime (R := Ideal.Fiber (Ideal.under R q) S) Q) (β :=
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) (Ideal.under R q)))
        (⇑φ₃ : (a : Localization.AtPrime Q) → Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q)))
    (inst : QuasiFiniteAt R (S := Ideal.Fiber (Ideal.under R q) S) Q),
    QuasiFinite.{u_1, u_2} R
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (Ideal.map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (Ideal.under R q)))
Tactic: obtain rfl := q.over_def p
Cleared hypotheses: p, inst_5, inst_6, Q, inst_7, hQ, inst_8, this_1, φ₁, φ₂, φ₃, this, inst