-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (hypothesis)
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)
⊢ QuasiFiniteAt A (S :=
    HasQuotient.Quotient (A ⊗[R] S) (B := Ideal (A ⊗[R] S))
      (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q)))
    (Ideal.map (F :=
      A ⊗[R] S →+*
        HasQuotient.Quotient (A ⊗[R] S) (B := Ideal (A ⊗[R] S))
          (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q)))
      (Ideal.Quotient.mk (Ideal.map (F := A →+* A ⊗[R] S) (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)
have this₁ : QuasiFiniteAt (HasQuotient.Quotient A (B := Ideal A) (Ideal.under A q)) (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))))
  (Ideal.map φ.toRingHom q)
Tactic: have := QuasiFiniteAt.baseChange (R := R) (S := _) (A := A ⧸ q.under A)
    (p.map (Ideal.Quotient.mk ((p.under R).map (algebraMap R S)))) (q.map φ.toRingHom) (by
    apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective
    rwa [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, sup_eq_left.mpr Ideal.map_comap_le,
      ← hφ₃, ← Ideal.comap_comap, Ideal.comap_map_of_surjective _ (by exact hφ₁),
      ← RingHom.ker_eq_comap_bot, hφ₂, sup_eq_left.mpr Ideal.map_comap_le])