awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
h₂ : Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤
⊢ Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤

Tactic:
use s.attach.biUnion sf

Premises used: Finset.biUnion, Finset.attach
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
⊢ Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤

Tactic:
(Algebra.adjoin_attach_biUnion (R := R) sf).trans _

Premises used: Algebra.adjoin_attach_biUnion, Eq.trans
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
h₂ : Eq.{u_2 + 1} (α := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) ⊤
⊢ Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤

Tactic:
convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _

Premises used: Algebra.adjoin_attach_biUnion, Eq.trans
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
h₂ : ∀ (x : S), Membership.mem (γ := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) x
⊢ Eq.{u_2 + 1} (α := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) ⊤

Tactic:
rw [eq_top_iff]

Premises used: Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
apply :
  ∀ (r : (↑(↑s : Set R) : Type u_1)),
    ∃ (n : ℕ),
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
          Submodule R S)
        ((↑r : R) ^ n • x)
⊢ Membership.mem (γ := Set (Set S))
      (Set.range fun (t : Subsemiring S) ↦
        ⋂ (_ :
          Membership.mem (γ := Set (Subsemiring S))
            {S_1 : Subsemiring S |
              Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S) ∪
                  sSup
                    (Set.image (α := Subalgebra R S) SetLike.coe
                      (Set.range fun (x : ↥s) ↦ adjoin R (↑(sf x) : Set S))) ⊆
                (↑S_1 : Set S)}
            t),
          (↑t : Set S))
      t →
    x ∈ t

Tactic:
apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
    _ hs _ _

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, iSup, Algebra.adjoin, SetLike.coe, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
rw :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ :=
    Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S)) ⊤
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
      Localization.Away (↑r : R) ⊗[R] S)
⊢ Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ :=
    Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
      Localization.Away (↑r : R) ⊗[R] S)

Tactic:
rw [s₂ r]
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
⊢ Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ :=
    Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S)) ⊤
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
      Localization.Away (↑r : R) ⊗[R] S)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
obtain :
  ∀ (n₁ : ℕ)
    (hn₁ :
      Membership.mem (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
        (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
        (HSMul.hSMul (β := Localization.Away (↑r : R) ⊗[R] S)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯)
          ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
            Localization.Away (↑r : R) ⊗[R] S))),
    ∃ (n : ℕ),
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
          Submodule R S)
        ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
        Submodule R S)
      ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
      (algebraMap S _ x) (by rw [s₂ r]; trivial)

Premises used: Algebra.algebraMap, Localization.Away, multiple_mem_adjoin_of_mem_localization_adjoin, SetLike.coe, Submonoid.powers, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    (HSMul.hSMul (β := Localization.Away (↑r : R) ⊗[R] S)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯)
      ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
        Localization.Away (↑r : R) ⊗[R] S))
⊢ Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)

Tactic:
rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁

Premises used: Submonoid.smul_def, map_mul, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
obtain :
  ∀ (n₂ : ℕ)
    (hn₂ :
      Membership.mem (γ := Subalgebra R S)
        (adjoin R
          (↑(IsLocalization.finsetIntegerMultiple
                (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
            Set S))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
          HMul.hMul (α := S)
            ((algebraMap R S : (a : R) → S)
                (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                      ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                  R) :
              S)
            x)),
    ∃ (n : ℕ),
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
          Submodule R S)
        ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
        Submodule R S)
      ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁

Premises used: IsLocalization.lift_mem_adjoin_finsetIntegerMultiple, Submonoid.powers, Subtype.val, rfl
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
      HMul.hMul (α := S)
        ((algebraMap R S : (a : R) → S)
            (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                  ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
              R) :
          S)
        x)
⊢ Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂

Premises used: pow_add, smul_smul, Submonoid.smul_def, Algebra.smul_def
-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
f : R →+* S := algebraMap R S
this :
  (r : ↥s) →
    Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S)
s₂ :
  ∀ (r : ↥s),
    Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
      (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
t : Set S
r : (↑(↑s : Set R) : Type u_1)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
    (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
    ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
        (HMul.hMul (α := S)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (↑r : R) ⊗[R] S)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Subalgebra R S)
    (adjoin R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
simp_rw [Submonoid.map_powers] at hn₂

Premises used: Submonoid.map_powers