-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 :
  QuasiFiniteAt R (S :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst_5 : CommRing A
inst_6 : Algebra R A
q : Ideal (A ⊗[R] S)
inst_7 : q.IsPrime
hq : p = Ideal.comap (F := S →+* A ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) q
φ : A ⊗[R] S →ₐ[A]
  TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
hφ₁ :
  Function.Surjective (α := A ⊗[R] S) (β :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (⇑φ : (a : A ⊗[R] S) → (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₂ :
  Eq (α := Ideal (A ⊗[R] S)) (RingHom.ker φ.toRingHom)
    (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))
hφ₃ :
  φ.comp (AlgHom.toRingHom TensorProduct.includeRight) =
    RingHom.comp (AlgHom.toRingHom TensorProduct.includeRight)
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
this :
  Ideal.IsPrime (α :=
    TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map φ.toRingHom q)
⊢ Eq (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p)
    (Ideal.comap (F :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)) →+*
        TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
      (AlgHom.toRingHom TensorProduct.includeRight) (Ideal.map φ.toRingHom q))
have a : Eq (α := Ideal S)
  (Ideal.comap (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.map (F :=
      S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))) p))
  (Ideal.comap (F :=
    S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)))
    (Ideal.comap (F :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p)) →+*
        TensorProduct.{u_1, u_4, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q))
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R p))))
      (AlgHom.toRingHom TensorProduct.includeRight) (Ideal.map φ.toRingHom q)))
Tactic: apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective