-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
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
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) ⋯;
    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))))
        ⋯;
    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 := φ₂) ⋯;
    ∀
      (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)))
⊢ 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

Premises used: Ideal.over_def, rfl