awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Algebra.IsIntegral R S
inst_8 : FiniteType R T
s : S
inst_9 : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := Subtype.mk (p := fun (x : S) ↦ x ∈ A) s ⋯
f : RingHom.{u_2, u_3} (Localization.Away sA) T := IsLocalization.Away.lift sA (g := algebraMap (↥A) T) ⋯
this_1 : Algebra.{u_2, u_3} (Localization.Away sA) T := f.toAlgebra
this_2 : Algebra (↥A) (Localization.Away sA) := OreLocalization.instAlgebra
this_3 : SMul (↥A) (Localization.Away sA) :=
  @toSMul _ _ (instCommSemiringAdjoinSingleton R s) OreLocalization.instSemiring _
this_4 : MulAction (↥A) (Localization.Away sA) := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
this_5 : IsScalarTower.{u_1, u_2, u_2} R (↥A) (Localization.Away sA)
this_6 : IsScalarTower.{u_2, u_2, u_3} (↥A) (Localization.Away sA) T
this_7 : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
this_8 : Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T
this_9 : Module.Finite.{u_2, u_3} (Localization.Away sA) T
this_10 : Module.Finite.{u_1, u_2} R ↥A
this : QuasiFinite.{u_1, u_2} R (Localization.Away sA)
⊢ QuasiFinite R T

Tactic:
exact .trans _ (Localization.Away sA) _
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
⊢ ∀ (r : R),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      (OneHom.toFun (M := Localization.AtPrime p)
        (↑(↑(Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq) :
              Localization.AtPrime p →* Localization.AtPrime q) :
          OneHom (Localization.AtPrime p) (Localization.AtPrime q))
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) r))
      ((algebraMap R (Localization.AtPrime (R := A ⊗[R] S) q) : (a : R) → Localization.AtPrime q) r)

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime p),
        IsScalarTower.algebraMap_apply R (A ⊗[R] S) (Localization.AtPrime q)]

Premises used: Localization.AtPrime, TensorProduct, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
h :
  ∀ (x : S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((AlgHom.comp (AlgHom.restrictScalars R (f.comp g)) TensorProduct.includeRight : (a : S) → Localization.AtPrime q)
          x :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((AlgHom.comp (B := A ⊗[R] S)
              (AlgHom.restrictScalars R (IsScalarTower.toAlgHom A (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q)))
              TensorProduct.includeRight :
            (a : S) → Localization.AtPrime q)
          x :
        Localization.AtPrime (R := A ⊗[R] S) q)
⊢ f.comp g = IsScalarTower.toAlgHom A (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q)

Tactic:
ext
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
x : S
⊢ Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
    ((AlgHom.comp (AlgHom.restrictScalars R (f.comp g)) TensorProduct.includeRight : (a : S) → Localization.AtPrime q)
        x :
      Localization.AtPrime (R := A ⊗[R] S) q)
    ((AlgHom.comp (B := A ⊗[R] S)
            (AlgHom.restrictScalars R (IsScalarTower.toAlgHom A (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q)))
            TensorProduct.includeRight :
          (a : S) → Localization.AtPrime q)
        x :
      Localization.AtPrime (R := A ⊗[R] S) q)

Tactic:
simp [f, g]
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
⊢ f.comp g = IsScalarTower.toAlgHom A (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q)

Tactic:
have : f.comp g = IsScalarTower.toAlgHom _ _ _ := by ext; simp [f, g]
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this : f.comp g = IsScalarTower.toAlgHom A (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q)
⊢ ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)

Tactic:
replace this (x : _) : f (g x) = algebraMap _ _ x := DFunLike.congr_fun this x
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
⊢ QuasiFiniteAt A (S := A ⊗[R] S) q

Tactic:
.of_forall_exists_mul_mem_range f fun x ↦ ?_

Premises used: Algebra.QuasiFinite.of_forall_exists_mul_mem_range
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
refine :
  ∀ (x : Localization.AtPrime (R := A ⊗[R] S) q),
    ∃ (s : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p)),
      IsUnit (M := Localization.AtPrime (R := A ⊗[R] S) q)
          ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s :
            Localization.AtPrime (R := A ⊗[R] S) q) ∧
        HMul.hMul (β := Localization.AtPrime (R := A ⊗[R] S) q) x
            ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s :
              Localization.AtPrime (R := A ⊗[R] S) q) ∈
          f.range
⊢ QuasiFiniteAt A (S := A ⊗[R] S) q

Tactic:
refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x : Localization.AtPrime (R := A ⊗[R] S) q
obtain :
  ∀ (x s : A ⊗[R] S) (hs : s ∈ q.primeCompl),
    ∃ (s_1 : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p)),
      IsUnit (M := Localization.AtPrime (R := A ⊗[R] S) q)
          ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
            Localization.AtPrime (R := A ⊗[R] S) q) ∧
        HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
            (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
                (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
              Localization.AtPrime (R := A ⊗[R] S) q)
            ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
              Localization.AtPrime (R := A ⊗[R] S) q) ∈
          f.range
⊢ ∃ (s : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p)),
    IsUnit (M := Localization.AtPrime (R := A ⊗[R] S) q)
        ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s :
          Localization.AtPrime (R := A ⊗[R] S) q) ∧
      HMul.hMul (β := Localization.AtPrime (R := A ⊗[R] S) q) x
          ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s :
            Localization.AtPrime (R := A ⊗[R] S) q) ∈
        f.range

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.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ ∃ (s_1 : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p)),
    IsUnit (M := Localization.AtPrime (R := A ⊗[R] S) q)
        ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
          Localization.AtPrime (R := A ⊗[R] S) q) ∧
      HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
          (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
              (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
            Localization.AtPrime (R := A ⊗[R] S) q)
          ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
            Localization.AtPrime (R := A ⊗[R] S) q) ∈
        f.range

Tactic:
⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩

Premises used: Eq.rec, Subtype.mk, And.intro, Exists.intro, IsLocalization.map_units, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
refine :
  HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
      (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
          (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) s) :
        Localization.AtPrime (R := A ⊗[R] S) q) ∈
    f.range
⊢ ∃ (s_1 : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p)),
    IsUnit (M := Localization.AtPrime (R := A ⊗[R] S) q)
        ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
          Localization.AtPrime (R := A ⊗[R] S) q) ∧
      HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
          (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
              (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
            Localization.AtPrime (R := A ⊗[R] S) q)
          ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q) s_1 :
            Localization.AtPrime (R := A ⊗[R] S) q) ∈
        f.range

Tactic:
refine ⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
rw :
  Membership.mem (α := Localization.AtPrime (R := A ⊗[R] S) q) f.range
    ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
      Localization.AtPrime (R := A ⊗[R] S) q)
⊢ HMul.hMul (α := Localization.AtPrime (R := A ⊗[R] S) q) (β := Localization.AtPrime (R := A ⊗[R] S) q)
      (IsLocalization.mk' (M := q.primeCompl) (Localization.AtPrime (R := A ⊗[R] S) q) x
          (Subtype.mk (p := fun (x : A ⊗[R] S) ↦ x ∈ q.primeCompl) s hs) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) s) :
        Localization.AtPrime (R := A ⊗[R] S) q) ∈
    f.range

Tactic:
rw [this, IsLocalization.mk'_spec_mk]

Premises used: IsLocalization.mk'_spec_mk
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
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 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
f : TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) →ₐ[A] Localization.AtPrime (R := A ⊗[R] S) q :=
  TensorProduct.lift (ofId A (Localization.AtPrime (R := A ⊗[R] S) q))
    { toRingHom := Localization.localRingHom p q (AlgHom.toRingHom TensorProduct.includeRight) hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] TensorProduct.{u_1, u_4, u_2} R A (Localization.AtPrime p) :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
this :
  ∀ (x : A ⊗[R] S),
    Eq (α := Localization.AtPrime (R := A ⊗[R] S) q)
      ((f : (a : A ⊗[R] Localization.AtPrime p) → Localization.AtPrime q)
          ((g : (a : A ⊗[R] S) → A ⊗[R] Localization.AtPrime p) x) :
        Localization.AtPrime (R := A ⊗[R] S) q)
      ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
        Localization.AtPrime (R := A ⊗[R] S) q)
x s : A ⊗[R] S
hs : s ∈ q.primeCompl
⊢ Membership.mem (α := Localization.AtPrime (R := A ⊗[R] S) q) f.range
    ((algebraMap (A ⊗[R] S) (Localization.AtPrime (R := A ⊗[R] S) q) : (a : A ⊗[R] S) → Localization.AtPrime q) x :
      Localization.AtPrime (R := A ⊗[R] S) q)

Tactic:
⟨g x, this x⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, DFunLike.coe