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 R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ ∃ a, φ₃ a = (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)

Tactic:
refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ 1 ⊗ₜ[R] s ∈ Q.primeCompl

case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
φ₁ : p.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ φ₃ (IsLocalization.mk' (Localization.AtPrime Q) (1 ⊗ₜ[R] x) ⟨1 ⊗ₜ[R] s, ?refine_1⟩) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R Sq) p)) (IsLocalization.mk' Sq x ⟨s, hs⟩)