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
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)
    (HSMul.hSMul (β := T) (HPow.hPow (α := Localization.Away sA) (Localization.Away.invSelf sA) n)
      ((algebraMap S T : (a : S) → T) x : T))

Tactic:
this.smul (Localization.Away.invSelf sA ^ n)

Premises used: Localization.Away.invSelf, IsIntegral.smul, HPow.hPow
-- 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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
h :
  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)
⊢ 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) ⋯))

Tactic:
convert! this.smul (Localization.Away.invSelf sA ^ n)

Premises used: Localization.Away.invSelf, IsIntegral.smul, HPow.hPow
-- 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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
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) ⋯) :
            S) :
        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)

Tactic:
rw [IsLocalization.mk'_eq_iff_eq_mul]

Premises used: IsLocalization.mk'_eq_iff_eq_mul
-- 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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
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)
⊢ (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)

Tactic:
simp only [map_pow, Algebra.smul_mul_assoc]

Premises used: map_pow, Algebra.smul_mul_assoc
-- 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
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)
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)
⊢ (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:
trans (sA • Localization.Away.invSelf sA) ^ n • (algebraMap S T x)

Premises used: Algebra.algebraMap, Localization.Away.invSelf, HSMul.hSMul, DFunLike.coe
-- 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
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 =
    HSMul.hSMul (β := T) (HSMul.hSMul (β := Localization.Away sA) sA (Localization.Away.invSelf sA) ^ n)
      ((algebraMap S T : (a : S) → T) x : T)

Tactic:
simp [Algebra.smul_def, -map_pow, Localization.Away.invSelf, Localization.mk_eq_mk']

Premises used: Localization.mk_eq_mk', Localization.Away.invSelf, map_pow, Algebra.smul_def
-- 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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
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 ⋯)) T :
                (a : Localization.Away ⟨s, ⋯⟩) → T)
              (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s ⋯)) :
            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 ⋯)) T :
              (a : Localization.Away ⟨s, ⋯⟩) → T)
            (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s ⋯)) :
          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)
⊢ 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:
simp only [Algebra.smul_def, map_pow, map_mul, mul_pow,
        ← IsScalarTower.algebraMap_apply, Subalgebra.algebraMap_def, sA]

Premises used: Subalgebra.algebraMap_def, map_pow, map_mul, Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply
-- 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
x : S
n : ℕ
this : IsIntegral.{u_2, u_3} (Localization.Away sA) (A := T) ((algebraMap S T : (a : S) → T) x : T)
⊢ 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 ⋯)) T :
                (a : Localization.Away ⟨s, ⋯⟩) → T)
              (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s ⋯)) :
            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 ⋯)) T :
              (a : Localization.Away ⟨s, ⋯⟩) → T)
            (Localization.Away.invSelf (Subtype.mk (p := fun (x : S) ↦ x ∈ A) s ⋯)) :
          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:
ring
-- 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 : IsScalarTower.{u_1, u_2, u_3} R (Localization.Away sA) T
⊢ 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
-- 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 : Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T
⊢ 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
-- 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 : Module.Finite.{u_2, u_3} (Localization.Away sA) T
⊢ Module.Finite.{u_1, u_2} R ↥A

Tactic:
have : Module.Finite R A :=
    Algebra.finite_adjoin_simple_of_isIntegral (Algebra.IsIntegral.isIntegral _)
-- 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 : Module.Finite.{u_1, u_2} R ↥A
⊢ QuasiFinite.{u_1, u_2} R (Localization.Away sA)

Tactic:
have : Algebra.QuasiFinite R (Localization.Away sA) := .of_isLocalization (.powers sA)
-- 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:
.trans _ (Localization.Away sA) _

Premises used: Localization.Away, Algebra.QuasiFinite.trans