awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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
⊢ ∃ (m : ↥M), m • x ∈ A
have 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
Tactic: obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
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')
⊢ ∃ (m : ↥M), m • x ∈ A
have 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')
Tactic: rw [Algebra.smul_def, ← map_mul] at hx''
Cleared hypotheses: hx''
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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')
⊢ ∃ (m : ↥M), m • x ∈ A
have obtain : ∀ (a : ↥M) (ha₂ : (↑a : S) * x' = (↑a : S) * ((↑y : S) ^ n * x)), ∃ (m : ↥M), m • x ∈ A
Tactic: obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx''
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ ∃ (m : ↥M), m • x ∈ A
have h : (a * y ^ n) • x ∈ A
Tactic: use a * y ^ n
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x ∈ A
have h : (a * y ^ n) • x = x' * (↑a : S)
Tactic: convert! A.mul_mem hx' (hA₂ a.prop) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h : (↑(a * y ^ n) : S) • x = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₁ : (↑(a * y ^ n) : S) * x = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₂ : (↑a : S) * (↑(y ^ n) : S) * x = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₃ : (↑a : S) * (↑y : S) ^ n * x = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₄ : (↑a : S) * ((↑y : S) ^ n * x) = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₅ : (↑a : S) * x' = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ (a * y ^ n) • x = x' * (↑a : S)
have h₆ : x' * (↑a : S) = x' * (↑a : S)
Tactic: rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
    mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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')
⊢ ∃ (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)
have 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) sorry :
          ↥(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: 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
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
have 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)
Tactic: refine ⟨⟨a, ha⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)
⊢ FiniteType R S
have obtain : ∀ (s_1 : Finset S) (h₁ : (↑s_1 : Set S) ⊆ s) (hs : Eq (α := Ideal S) (Ideal.span (↑s_1 : Set S)) ⊤), FiniteType R S
Tactic: obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
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)) ⊤
⊢ FiniteType R S
have h₂ : ∀ (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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
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))
⊢ FiniteType R S
have h₂ : ∀ (r : ↥s), Subalgebra.FG.{u_1, u_2} (R := R) (A := Localization.Away (↑r : S)) ⊤
Tactic: replace h := fun r => (h r).1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)) ⊤
⊢ FiniteType R S
have 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
Tactic: choose t ht using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)))) ⊤
⊢ Membership.mem (γ := Ideal S) (Ideal.span (↑s : Set S)) 1
have rw : Membership.mem (γ := Ideal S) ⊤ 1
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
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)))) ⊤
⊢ FiniteType R S
have obtain : ∀ (l : (↑(↑s : Set S) : Type u_2) →₀ S)
  (hl :
    Eq (α := S)
      ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
            (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
          l :
        S)
      (1 : S)),
  FiniteType R S
Tactic: obtain ⟨l, hl⟩ :=
    (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)