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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
⊢ (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)

Tactic:
have hx₁ : (y : S) • (s : Set S') = g '' _ :=
    (IsLocalization.finsetIntegerMultiple_image _ s).symm
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
rw : (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑(Subalgebra.map g A) : Set S')
⊢ (↑y : S) • (↑s : Set S') ⊆ (↑(Subalgebra.map g A) : Set S')

Tactic:
rw [hx₁]
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
⊢ (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑(Subalgebra.map g A) : Set S')

Tactic:
Set.image_mono hA₁

Premises used: Set.image_mono, setOf, Set.image
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
⊢ (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑(Subalgebra.map g A) : Set S')

Tactic:
exact Set.image_mono hA₁

Premises used: Set.image_mono
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A),
    ∃ (m : ↥M), m • x ∈ A
⊢ ∃ (m : ↥M), m • x ∈ A

Tactic:
obtain ⟨n, hn⟩ :=
    Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g)
      (by rw [hx₁]; exact Set.image_mono hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2))

Premises used: Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin, Subalgebra.map, SetLike.coe, Set.mem_image_of_mem, Subtype.val, Subtype.property
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
obtain :
  ∀ (x' : S) (hx' : x' ∈ (↑A.toSubsemiring : Set S))
    (hx'' :
      ((↑g : S →+* S') : (a : S) → S') x' =
        HSMul.hSMul (β := S') ((↑y : S) ^ n) ((algebraMap S S' : (a : S) → S') x : S')),
    ∃ (m : ↥M), m • x ∈ A
⊢ ∃ (m : ↥M), m • x ∈ A

Tactic:
obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl)

Premises used: le_of_eq, 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  ((↑g : S →+* S') : (a : S) → S') x' = HSMul.hSMul (β := S') ((↑y : S) ^ n) ((algebraMap S S' : (a : S) → S') x : S')
⊢ Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')

Tactic:
rw [Algebra.smul_def, ← map_mul] at hx''

Premises used: map_mul, 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')
obtain : ∀ (a : ↥M) (ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)), ∃ (m : ↥M), m • x ∈ A
⊢ ∃ (m : ↥M), m • x ∈ A

Tactic:
obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx''

Premises used: Iff.mp, IsLocalization.eq_iff_exists
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')
a : ↥M
ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)
h : (a * y ^ n) • x ∈ A
⊢ ∃ (m : ↥M), m • x ∈ A

Tactic:
use a * y ^ n
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')
a : ↥M
ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)
⊢ x' * (↑a : S) ∈ A

Tactic:
A.mul_mem hx' (hA₂ a.prop)

Premises used: Subalgebra.mul_mem, Subtype.prop
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')
a : ↥M
ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)
h : (a * y ^ n) • x = x' * (↑a : S)
⊢ (a * y ^ n) • x ∈ A

Tactic:
convert! A.mul_mem hx' (hA₂ a.prop) using 1

Premises used: Subalgebra.mul_mem, Subtype.prop
-- 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' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
n : ℕ
hn : ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ (↑A.toSubsemiring : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') (((↑g : S →+* S') : (a : S) → S') x' : S')
    ((algebraMap S S' : (a : S) → S') ((↑y : S) ^ n * x) : S')
a : ↥M
ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)
h : (↑(a * y ^ n) : S) • x = x' * (↑a : S)
h₁ : (↑(a * y ^ n) : S) * x = x' * (↑a : S)
h₂ : (↑a : S) * (↑(y ^ n) : S) * x = x' * (↑a : S)
h₃ : (↑a : S) * (↑y : S) ^ n * x = x' * (↑a : S)
h₄ : (↑a : S) * ((↑y : S) ^ n * x) = x' * (↑a : S)
h₅ : (↑a : S) * x' = x' * (↑a : S)
h₆ h₇ : x' * (↑a : S) = x' * (↑a : S)
⊢ (a * y ^ n) • x = x' * (↑a : S)

Tactic:
rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]

Premises used: mul_assoc, Submonoid.smul_def, SubmonoidClass.coe_pow, mul_comm, smul_eq_mul, Submonoid.coe_mul
-- 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
a : R
left : a ∈ (↑M : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S)
    (Subsemiring.toSubmonoid
      (Subalgebra.toSubsemiring
        (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))))
    ((algebraMap R S : (a : R) → S) a : S)

Tactic:
Subalgebra.algebraMap_mem _ a

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
a : R
left : a ∈ (↑M : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S)
    (Subsemiring.toSubmonoid
      (Subalgebra.toSubsemiring
        (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))))
    ((algebraMap R S : (a : R) → S) a : S)

Tactic:
exact Subalgebra.algebraMap_mem _ a

Premises used: Subalgebra.algebraMap_mem
-- 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
obtain :
  ∀ (a : R) (ha : a ∈ (↑M : Set R))
    (e :
      Membership.mem (γ := Subalgebra R S)
        (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
        (HSMul.hSMul (α := ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
          (Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯ :
            ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
          x)),
    ∃ (m : ↥M),
      Membership.mem (γ := Subalgebra R S)
        (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
        (m • x)
⊢ ∃ (m : ↥M),
    Membership.mem (γ := Subalgebra R S)
      (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (m • x)

Tactic:
obtain ⟨⟨_, a, ha, rfl⟩, e⟩ :=
    IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _)
      Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx

Premises used: Algebra.algebraMap, Algebra.subset_adjoin, Algebra.adjoin, Submonoid.map, IsLocalization.exists_smul_mem_of_mem_adjoin, 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
a : R
ha : a ∈ (↑M : Set R)
e :
  Membership.mem (γ := Subalgebra R S)
    (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    (HSMul.hSMul (α := ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      (Subtype.mk (p := fun (x : S) ↦
          Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
          ((algebraMap R S : (a : R) → S) a) ⋯ :
        ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      x)
⊢ ∃ (m : ↥M),
    Membership.mem (γ := Subalgebra R S)
      (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (m • x)

Tactic:
⟨⟨a, ha⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro
-- 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
a : R
ha : a ∈ (↑M : Set R)
e :
  Membership.mem (γ := Subalgebra R S)
    (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    (HSMul.hSMul (α := ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      (Subtype.mk (p := fun (x : S) ↦
          Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
          ((algebraMap R S : (a : R) → S) a) ⋯ :
        ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      x)
refine :
  Membership.mem (γ := Subalgebra R S)
    (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha • x)
⊢ ∃ (m : ↥M),
    Membership.mem (γ := Subalgebra R S)
      (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (m • x)

Tactic:
refine ⟨⟨a, ha⟩, ?_⟩
-- 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
M : Submonoid R
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
a : R
ha : a ∈ (↑M : Set R)
e :
  Membership.mem (γ := Subalgebra R S)
    (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    (HSMul.hSMul (α := ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      (Subtype.mk (p := fun (x : S) ↦
          Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
          ((algebraMap R S : (a : R) → S) a) ⋯ :
        ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M))
      x)
⊢ Membership.mem (γ := Subalgebra R S)
    (Algebra.adjoin R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha • x)

Tactic:
simpa only [Submonoid.smul_def, algebraMap_smul] using e

Premises used: algebraMap_smul, Submonoid.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 : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, FiniteType.{u_1, u_2} R (Localization.Away x)
obtain :
  ∀ (s_1 : Finset S) (h₁ : (↑s_1 : Set S) ⊆ s) (hs : Eq (α := Ideal S) (Ideal.span (↑s_1 : Set S)) ⊤), FiniteType R S
⊢ FiniteType R S

Tactic:
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- 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 S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
h : ∀ x ∈ s_1, FiniteType.{u_1, u_2} R (Localization.Away x)
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
⊢ ∀ (i : ↥s), FiniteType.{u_1, u_2} R (Localization.Away (↑i : S))

Tactic:
replace h (i : s) : Algebra.FiniteType R (Localization.Away i.val) := h i (h₁ i.property)
-- 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 S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FiniteType.{u_1, u_2} R (Localization.Away (↑i : S))
⊢ ∀ (r : ↥s), Subalgebra.FG.{u_1, u_2} (R := R) (A := Localization.Away (↑r : S)) ⊤

Tactic:
replace h := fun r => (h r).1
-- 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 S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (r : ↥s), Subalgebra.FG.{u_1, u_2} (R := R) (A := Localization.Away (↑r : S)) ⊤
choose :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤),
    FiniteType R S
⊢ FiniteType R S

Tactic:
choose t ht using h
-- 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 S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
t : (r : ↥s) → Finset (Localization.Away (↑r : S))
ht :
  ∀ (r : ↥s),
    Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤
rw : Membership.mem (γ := Ideal S) ⊤ 1
⊢ Membership.mem (γ := Ideal S) (Ideal.span (↑s : Set S)) 1

Tactic:
rw [hs]