Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this✝¹ : (Ideal.map φ.toRingHom q).IsPrime
this✝ : QuasiFiniteAt (A ⧸ Ideal.under A q) (Ideal.map φ.toRingHom q)
this : QuasiFiniteAt A (Ideal.map φ.toRingHom q)
e : (A ⊗[R] S ⧸ Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)) ≃ₐ[A]
  (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  ((Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)).quotientEquivAlg (RingHom.ker φ) AlgEquiv.refl ⋯).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)
⊢ QuasiFiniteAt A (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)

Tactic:
refine .of_surjectiveOnStalks (q.map φ.toRingHom) e.symm.toAlgHom
    e.symm.toRingEquiv.surjectiveOnStalks _ ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this✝¹ : (Ideal.map φ.toRingHom q).IsPrime
this✝ : QuasiFiniteAt (A ⧸ Ideal.under A q) (Ideal.map φ.toRingHom q)
this : QuasiFiniteAt A (Ideal.map φ.toRingHom q)
e : (A ⊗[R] S ⧸ Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)) ≃ₐ[A]
  (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  ((Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)).quotientEquivAlg (RingHom.ker φ) AlgEquiv.refl ⋯).trans
    (Ideal.quotientKerAlgEquivOfSurjective hφ₁)
⊢ Ideal.map φ.toRingHom q =
    Ideal.comap (↑e.symm).toRingHom
      (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q))) q)