awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
trans :
  (algebraMap S T : (a : S) → T) x =
    HSMul.hSMul (β := T) (HSMul.hSMul (β := Localization.Away sA) sA (Localization.Away.invSelf sA) ^ n)
      ((algebraMap S T : (a : S) → T) x : T)
⊢ (algebraMap S T : (a : S) → T) x =
    HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n •
      HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) x : T)
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) n)
have trans₁ : HSMul.hSMul (β := T) (HSMul.hSMul (β := Localization.Away sA) sA (Localization.Away.invSelf sA) ^ n)
    ((algebraMap S T : (a : S) → T) x : T) =
  HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n •
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) x : T)
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) n)
Tactic: trans (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T x)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
⊢ HSMul.hSMul (β := T) (HSMul.hSMul (β := Localization.Away sA) sA (Localization.Away.invSelf sA) ^ n)
      ((algebraMap S T : (a : S) → T) x : T) =
    HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n •
      HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) x : T)
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) n)
have simp : HMul.hMul (β := T)
    (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) n *
      HPow.hPow (α := T)
        ((algebraMap (Localization.Away (M := ↥A) (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s sorry)) T :
              (a : Localization.Away ⟨s, sorry⟩) → T)
            (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s sorry)) :
          T)
        n)
    ((algebraMap S T : (a : S) → T) x : T) =
  HPow.hPow (α := T)
      ((algebraMap (Localization.Away (M := ↥A) (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s sorry)) T :
            (a : Localization.Away ⟨s, sorry⟩) → T)
          (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s sorry)) :
        T)
      n *
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) x : T)
      (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) s : T) n)
Tactic: simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
⊢ QuasiFinite R T
have this₁ : Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T
Tactic: have : Algebra.IsIntegral (Localization.Away sA) T := by
    refine ⟨fun x ↦ ?_⟩
    obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x
    have : _root_.IsIntegral (Localization.Away sA) (algebraMap S T x) :=
      (Algebra.IsIntegral.isIntegral (R := R) x).algebraMap.tower_top
    convert! this.smul (Localization.Away.invSelf sA ^ n)
    rw [IsLocalization.mk'_eq_iff_eq_mul]
    simp only [map_pow, Algebra.smul_mul_assoc]
    trans (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T x)
    · simp [Algebra.smul_def, -map_pow, Localization.Away.invSelf, Localization.mk_eq_mk']
    · simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]
      ring
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 : Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T
⊢ QuasiFinite R T
have this₁ : Module.Finite.{u_2, u_3} (Localization.Away sA) T
Tactic: have : Module.Finite (Localization.Away sA) T :=
    have : Algebra.FiniteType (Localization.Away sA) T := .of_restrictScalars_finiteType R _ _
    Algebra.IsIntegral.finite
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 : Module.Finite.{u_2, u_3} (Localization.Away sA) T
⊢ QuasiFinite R T
have this₁ : Module.Finite.{u_1, u_2} R ↥A
Tactic: have : Module.Finite R A :=
    Algebra.finite_adjoin_simple_of_isIntegral (Algebra.IsIntegral.isIntegral _)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (hypothesis)
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 : Module.Finite.{u_1, u_2} R ↥A
⊢ QuasiFinite R T
have this₁ : QuasiFinite.{u_1, u_2} R (Localization.Away sA)
Tactic: have : Algebra.QuasiFinite R (Localization.Away sA) := .of_isLocalization (.powers sA)
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (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 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))
⊢ QuasiFiniteAt A (S := A ⊗[R] S) q
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (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 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)
⊢ QuasiFiniteAt A (S := A ⊗[R] S) q
have 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)
Tactic: replace this (x : _) : f (g x) = algebraMap _ _ x := DFunLike.congr_fun this x
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
have 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
Tactic: refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Basic (goal)
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
have 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
Tactic: refine ⟨g s, this s ▸ IsLocalization.map_units _ ⟨s, hs⟩, ?_⟩