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 : QuasiFinite R S
P : Ideal R
inst_8 : P.IsPrime
Q : Ideal S
inst_9 : Q.IsPrime
inst_10 : Q.LiesOver P
inst_11 : Algebra.{u_1, u_2} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra P Q
⊢ Module.Finite.{u_1, u_2} P.ResidueField Q.ResidueField

Tactic:
have : QuasiFinite P.ResidueField Q.ResidueField := .of_restrictScalars R _ _
  .of_quasiFinite

Premises used: Algebra.QuasiFinite.of_restrictScalars, Ideal.ResidueField, Module.Finite.of_quasiFinite
-- 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
inst_3 : FiniteType R S
⊢ QuasiFinite R S ↔
    ∀ (x : PrimeSpectrum R),
      Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})

Tactic:
⟨fun H _ ↦ finite_comap_preimage_singleton _, fun H ↦ ⟨fun P _ ↦ ?_⟩⟩

Premises used: Algebra.QuasiFinite.mk, Algebra.QuasiFinite.finite_comap_preimage_singleton, Iff.intro
-- 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
inst_3 : FiniteType R S
refine :
  ∀
    (H :
      ∀ (x : PrimeSpectrum R),
        Set.Finite (α := PrimeSpectrum S)
          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x}))
    (P : Ideal R) (x : P.IsPrime), Module.Finite P.ResidueField (P.Fiber S)
⊢ QuasiFinite R S ↔
    ∀ (x : PrimeSpectrum R),
      Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {x})

Tactic:
refine ⟨fun H _ ↦ finite_comap_preimage_singleton _, fun H ↦ ⟨fun P _ ↦ ?_⟩⟩
-- 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
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
rw : IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)
⊢ Module.Finite P.ResidueField (P.Fiber S)

Tactic:
rw [Module.finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero]

Premises used: Module.finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero
-- 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
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
⊢ IsJacobsonRing (P.Fiber S)

Tactic:
have : IsJacobsonRing (P.Fiber S) := isJacobsonRing_of_finiteType (A := P.ResidueField)
-- 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
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)
⊢ Finite (PrimeSpectrum (P.Fiber S))

Tactic:
have : Finite (PrimeSpectrum (P.Fiber S)) :=
    (PrimeSpectrum.preimageEquivFiber R S ⟨P, ‹_›⟩).finite_iff.mp (H ⟨P, ‹_›⟩)
-- 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
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_1 : IsJacobsonRing (P.Fiber S)
this : Finite (PrimeSpectrum (P.Fiber S))
⊢ IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)

Tactic:
⟨Algebra.FiniteType.isNoetherianRing P.ResidueField _,
    (PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero.mp inferInstance).right⟩

Premises used: PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, Algebra.FiniteType.isNoetherianRing, Ideal.ResidueField, inferInstance, And.right, And.intro, Iff.mp
-- 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
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_1 : IsJacobsonRing (P.Fiber S)
this : Finite (PrimeSpectrum (P.Fiber S))
⊢ IsNoetherianRing (P.Fiber S) ∧ Ring.KrullDimLE 0 (P.Fiber S)

Tactic:
exact ⟨Algebra.FiniteType.isNoetherianRing P.ResidueField _,
    (PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero.mp inferInstance).right⟩
-- 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
inst_3 : FiniteType R S
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)
⊢ QuasiFinite R S ↔ ∀ (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]

Premises used: Equiv.forall_congr_left, PrimeSpectrum.equivSubtype, Subtype.forall, Algebra.QuasiFinite.iff_finite_comap_preimage_singleton, RelIso.toEquiv
-- 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
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)

Tactic:
forall₂_congr fun I hI ↦ ?_

Premises used: forall₂_congr
-- 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
inst_3 : FiniteType R S
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)
⊢ (∀ (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:
refine forall₂_congr fun I hI ↦ ?_

Premises used: forall₂_congr
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
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)
⊢ 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:
rw [← Set.finite_image_iff (Function.Injective.injOn fun _ _ ↦ PrimeSpectrum.ext)]

Premises used: PrimeSpectrum.ext, Function.Injective.injOn, Set.finite_image_iff
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
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)
⊢ 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:
congr!
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
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
⊢ 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:
ext J
-- 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
inst_3 : FiniteType R S
I : Ideal R
hI : I.IsPrime
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:
simp [(PrimeSpectrum.equivSubtype S).exists_congr_left, PrimeSpectrum.ext_iff, eq_comm,
    PrimeSpectrum.equivSubtype, Ideal.primesOver, and_comm, Ideal.liesOver_iff, Ideal.under]

Premises used: Equiv.exists_congr_left, Ideal.primesOver, Ideal.liesOver_iff, PrimeSpectrum.equivSubtype, and_comm, eq_comm, PrimeSpectrum.ext_iff, RelIso.toEquiv, Ideal.under
-- 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]
⊢ Membership.mem (γ := Set S) {s} s

Tactic:
simp
-- 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 : MulAction (↥A) (Localization.Away sA) := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
⊢ IsScalarTower.{u_1, u_2, u_2} R (↥A) (Localization.Away sA)

Tactic:
have : IsScalarTower R A (Localization.Away sA) := OreLocalization.instIsScalarTower
-- 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 : IsScalarTower.{u_1, u_2, u_2} R (↥A) (Localization.Away sA)
⊢ 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])
-- 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 : IsScalarTower.{u_2, u_2, u_3} (↥A) (Localization.Away sA) T
⊢ 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
-- 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:
⟨fun x ↦ ?_⟩

Premises used: Algebra.IsIntegral.mk
-- 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
refine : ∀ (x : T), IsIntegral.{u_2, u_3} (Localization.Away sA) x
⊢ Algebra.IsIntegral.{u_2, u_3} (Localization.Away sA) T

Tactic:
refine ⟨fun x ↦ ?_⟩
-- 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
x : T
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) ⋯))
⊢ IsIntegral.{u_2, u_3} (Localization.Away sA) x

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- 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
x : S
n : ℕ
⊢ 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