R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Monoid.FG { x // x ∈ invSubmonoid M S }
⊢ Algebra.FiniteType R S
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
⊢ Algebra.FiniteType R S
have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Submonoid.FG (invSubmonoid M S)
⊢ Algebra.FiniteType R S
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Monoid.FG { x // x ∈ invSubmonoid M S }
⊢ Algebra.FiniteType R S
rw [Monoid.fg_iff_submonoid_fg] at this
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.FiniteType R S
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Submonoid.FG (invSubmonoid M S)
⊢ Algebra.FiniteType R S
rcases this with ⟨s, hs⟩
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.adjoin R ↑s = ⊤
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.FiniteType R S
refine' ⟨⟨s, _⟩⟩
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ ⊤ ≤ Algebra.adjoin R ↑s
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.adjoin R ↑s = ⊤
rw [eq_top_iff]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ Algebra.adjoin R ↑s
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ ⊤ ≤ Algebra.adjoin R ↑s
rintro x -
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ Algebra.adjoin R ↑s
change x ∈ (Subalgebra.toSubmodule (Algebra.adjoin R _ : Subalgebra R S) : Set S)
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]
no goals
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.287534
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤
trivial