awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : FiniteType R S
H :
  ∀ (x : PrimeSpectrum R),
    Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})
P : Ideal R
h : P.IsPrime
this : IsJacobsonRing (P.Fiber S)
⊢ IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)
have this₁ : Finite (PrimeSpectrum (P.Fiber S))
Tactic: have : Finite (PrimeSpectrum (P.Fiber S)) :=
    (PrimeSpectrum.preimageEquivFiber R S ⟨P, ‹_›⟩).finite_iff.mp (H ⟨P, ‹_›⟩)
-- 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
inst_3 : FiniteType R S
⊢ QuasiFinite R S ↔ ∀ (I : Ideal R), I.IsPrime → Set.Finite (α := Ideal S) (I.primesOver S)
have rw : (∀ (a : Ideal R) (b : a.IsPrime),
    Set.Finite (α := PrimeSpectrum S)
      (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        (singleton (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
            PrimeSpectrum R)))) ↔
  ∀ (I : Ideal R), I.IsPrime → Set.Finite (α := Ideal S) (I.primesOver S)
Tactic: rw [iff_finite_comap_preimage_singleton,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall]
-- 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
inst_3 : FiniteType R S
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      Set.Finite (α := PrimeSpectrum S)
        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          (singleton (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
              PrimeSpectrum R)))) ↔
    ∀ (I : Ideal R), I.IsPrime → Set.Finite (α := Ideal S) (I.primesOver S)
have refine : ∀ (I : Ideal R) (hI : I.IsPrime),
  Set.Finite (α := PrimeSpectrum S)
      (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        (singleton (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
            PrimeSpectrum R))) ↔
    Set.Finite (α := Ideal S) (I.primesOver S)
Tactic: refine forall₂_congr fun I hI ↦ ?_
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
⊢ Set.Finite (α := PrimeSpectrum S)
      (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        (singleton (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
            PrimeSpectrum R))) ↔
    Set.Finite (α := Ideal S) (I.primesOver S)
have rw : Set.Finite (α := Ideal S)
    ((fun (x : PrimeSpectrum S) ↦ x.asIdeal) ''
      Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        (singleton (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
            PrimeSpectrum R))) ↔
  Set.Finite (α := Ideal S) (I.primesOver S)
Tactic: rw [← Set.finite_image_iff (Function.Injective.injOn fun _ _ ↦ PrimeSpectrum.ext)]
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
⊢ Set.Finite (α := Ideal S)
      ((fun (x : PrimeSpectrum S) ↦ x.asIdeal) ''
        Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          (singleton (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
              PrimeSpectrum R))) ↔
    Set.Finite (α := Ideal S) (I.primesOver S)
have a : Eq (α := Set (Ideal S))
  ((fun (x : PrimeSpectrum S) ↦ x.asIdeal) ''
    Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
      (singleton (α := PrimeSpectrum R)
        ((Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
          PrimeSpectrum R)))
  (I.primesOver S)
Tactic: congr!
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
⊢ Eq (α := Set (Ideal S))
    ((fun (x : PrimeSpectrum S) ↦ x.asIdeal) ''
      Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
        (singleton (α := PrimeSpectrum R)
          ((Equiv.symm
                  (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                    fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
              (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
            PrimeSpectrum R)))
    (I.primesOver S)
have a : ∀ (J : Ideal S),
  Membership.mem (γ := Set (Ideal S))
      ((fun (x : PrimeSpectrum S) ↦ x.asIdeal) ''
        Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
          (singleton (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) I hI) :
              PrimeSpectrum R)))
      J ↔
    Membership.mem (γ := Set (Ideal S)) (I.primesOver S) J
Tactic: ext J
-- 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 : MulAction (↥A) (Localization.Away sA) := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
⊢ QuasiFinite R T
have this₁ : IsScalarTower.{u_1, u_2, u_2} R (↥A) (Localization.Away sA)
Tactic: have : IsScalarTower R A (Localization.Away sA) := OreLocalization.instIsScalarTower
-- 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 : IsScalarTower.{u_1, u_2, u_2} R (↥A) (Localization.Away sA)
⊢ QuasiFinite R T
have this₁ : IsScalarTower.{u_2, u_2, u_3} (↥A) (Localization.Away sA) T
Tactic: have : IsScalarTower A (Localization.Away sA) T :=
    .of_algebraMap_eq (by simp [f, RingHom.algebraMap_toAlgebra, A])
-- 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 : IsScalarTower.{u_2, u_2, u_3} (↥A) (Localization.Away sA) T
⊢ QuasiFinite R T
have this₁ : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
Tactic: have : IsScalarTower R (Localization.Away sA) T := .to₁₃₄ R A (Localization.Away sA) T
-- 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 : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
⊢ Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T
have refine : ∀ (x : T), IsIntegral.{u_2, u_3} (Localization.Away sA) x
Tactic: refine ⟨fun 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 : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
x : T
⊢ IsIntegral.{u_2, u_3} (Localization.Away sA) x
have obtain : ∀ (x : S) (n : ℕ),
  IsIntegral.{u_2, u_3} (Localization.Away sA)
    (IsLocalization.mk' T x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) sorry))
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x
Cleared hypotheses: x
-- 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
x : S
n : ℕ
⊢ IsIntegral.{u_2, u_3} (Localization.Away sA)
    (IsLocalization.mk' T x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯))
have this₁ : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
Tactic: have : _root_.IsIntegral (Localization.Away sA) (algebraMap S T x) :=
      (Algebra.IsIntegral.isIntegral (R := R) x).algebraMap.tower_top
-- 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)
⊢ IsIntegral.{u_2, u_3} (Localization.Away sA)
    (IsLocalization.mk' T x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯))
have h : IsLocalization.mk' T x
    (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x) ((fun (x : ℕ) ↦ s ^ x) n)
      sorry) =
  HSMul.hSMul (β := T) (HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n)
    ((algebraMap S T : (a : S) → T) x : T)
Tactic: convert! this.smul (Localization.Away.invSelf sA ^ n)
-- 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)
⊢ IsLocalization.mk' T x
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯) =
    HSMul.hSMul (β := T) (HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n)
      ((algebraMap S T : (a : S) → T) x : T)
have h : (algebraMap S T : (a : S) → T) x =
  HMul.hMul (β := T)
    (HSMul.hSMul (β := T) (HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n)
      ((algebraMap S T : (a : S) → T) x : T))
    ((algebraMap S T : (a : S) → T)
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
              ((fun (x : ℕ) ↦ s ^ x) n) sorry) :
          S) :
      T)
Tactic: rw [IsLocalization.mk'_eq_iff_eq_mul]
-- 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)
⊢ (algebraMap S T : (a : S) → T) x =
    HMul.hMul (β := T)
      (HSMul.hSMul (β := T) (HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n)
        ((algebraMap S T : (a : S) → T) x : T))
      ((algebraMap S T : (a : S) → T)
          (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers s) x)
                ((fun (x : ℕ) ↦ s ^ x) n) ⋯) :
            S) :
        T)
have h : (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)
Tactic: simp only [map_pow, Algebra.smul_mul_assoc]
-- 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)
⊢ (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 : (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)
Tactic: trans (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T x)