awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
suffices : s ∉ q
⊢ IsUnit.{u_2} (M := HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((φ₂ : (a : p.Fiber S) → Sq ⧸ Ideal.map (algebraMap R Sq) p) (1 ⊗ₜ[R] s) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
suffices s ∉ q by
        have := (IsLocalization.map_units (M := q.primeCompl) Sq ⟨_, this⟩).map
          (algebraMap _ (Sq ⧸ p.map (algebraMap R Sq)))
        simpa [φ₂, ← IsScalarTower.algebraMap_apply] using this
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
this : HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q
⊢ s ∉ q

Tactic:
simpa [← hQ, ← H, Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
suffices : HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q
⊢ s ∉ q

Tactic:
suffices algebraMap _ _ r * y ∉ Q by simpa [← hQ, ← H, Algebra.smul_def]
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
⊢ HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q

Tactic:
Q.primeCompl.mul_mem ?_ hy

Premises used: Submonoid.mul_mem, Set.Mem, setOf, Ideal.primeCompl, Not
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
refine : Membership.mem (α := p.Fiber S) Q.primeCompl ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S)
⊢ HMul.hMul (α := p.Fiber S) ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S) y ∉ Q

Tactic:
refine Q.primeCompl.mul_mem ?_ hy

Premises used: Submonoid.mul_mem, Ideal.primeCompl
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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)))
    ⋯
y : p.Fiber S
hy : y ∈ Q.primeCompl
r : R
hrp : r ∉ p
s : S
H : r • y = 1 ⊗ₜ[R] s
⊢ Membership.mem (α := p.Fiber S) Q.primeCompl ((algebraMap R (p.Fiber S) : (a : R) → p.Fiber S) r : p.Fiber S)

Tactic:
simpa only [Ideal.mem_primeCompl_iff, ← Ideal.mem_comap, ← Q.over_def p]

Premises used: Ideal.mem_primeCompl_iff, Ideal.over_def, Ideal.mem_comap
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
x : Sq
obtain :
  ∀ (x s : S) (hs : s ∈ q.primeCompl),
    ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
      Eq.{u_2 + 1} (α := 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) a :
          HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
              (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
            (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
          HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := 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) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          x :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := 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) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

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

Premises used: Subtype.mk, IsLocalization.mk', Exists.intro, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
refine_1 : 1 ⊗ₜ[R] s ∈ Q.primeCompl
refine_2 :
  Eq (α := 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)
        (IsLocalization.mk' (M := Q.primeCompl) (Localization.AtPrime (R := p.Fiber S) Q) (1 ⊗ₜ[R] x)
          (Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) (1 ⊗ₜ[R] s) ⋯)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) : (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
⊢ ∃ (a : Localization.AtPrime (R := p.Fiber S) Q),
    Eq.{u_2 + 1} (α := 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) a :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) :
            (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
          (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
        HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ 1 ⊗ₜ[R] s ∈ Q.primeCompl

Tactic:
simpa [← hQ] using hs
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ Eq (α := 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)
        (IsLocalization.mk' (M := Q.primeCompl) (Localization.AtPrime (R := p.Fiber S) Q) (1 ⊗ₜ[R] x)
          (Subtype.mk (p := fun (x : p.Fiber S) ↦ x ∈ Q.primeCompl) (1 ⊗ₜ[R] s) ⋯)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p) : (a : Sq) → Sq ⧸ Ideal.map (algebraMap R Sq) p)
        (IsLocalization.mk' Sq x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hs)) :
      HasQuotient.Quotient Sq (B := Ideal Sq) (Ideal.map (F := R →+* Sq) (algebraMap R Sq) p))

Tactic:
simp [φ₃, IsLocalization.lift_mk'_spec, φ₂, IsScalarTower.algebraMap_apply S Sq (Sq ⧸ _),
        -Ideal.Quotient.mk_algebraMap, ← map_mul]

Premises used: IsLocalization.lift_mk'_spec, HasQuotient.Quotient, map_mul, IsScalarTower.algebraMap_apply, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.QuasiFinite.Weakly
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.IsPrime
inst_4 : p.IsPrime
inst_5 : q.LiesOver p
Q : Ideal (p.Fiber S)
inst_6 : Q.IsPrime
hQ : Ideal.comap (F := S →+* TensorProduct R p.ResidueField S) (AlgHom.toRingHom TensorProduct.includeRight) Q = q
inst_7 : QuasiFiniteAt p.ResidueField (S := p.Fiber S) Q
Sq : Type u_2 := Localization.AtPrime q
this : 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 := φ₂) ⋯
⊢ 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)

Tactic:
have : Function.Surjective φ₃ := by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
    refine ⟨IsLocalization.mk' (M := Q.primeCompl) _ (1 ⊗ₜ x) ⟨1 ⊗ₜ s, ?_⟩, ?_⟩
    · simpa [← hQ] using hs
    · simp [φ₃, IsLocalization.lift_mk'_spec, φ₂, IsScalarTower.algebraMap_apply S Sq (Sq ⧸ _),
        -Ideal.Quotient.mk_algebraMap, ← map_mul]