[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.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_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ ↑(algebraMap R S) a ∈ IsUnit.submonoid S
[PROOFSTEP]
exact IsLocalization.map_units S ⟨_, ha⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ m • ↑(↑(toInvSubmonoid M S) m) = 1
[PROOFSTEP]
convert mul_toInvSubmonoid M S m
[GOAL]
case h.e'_2.h.e
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ HSMul.hSMul m = HMul.hMul (↑(algebraMap R S) ↑m)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑(algebraMap R S) ↑m * x✝
[PROOFSTEP]
rw [← Algebra.smul_def]
[GOAL]
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑m • x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
refine' ⟨r, m, _⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
rw [Algebra.smul_def, ← e, mul_assoc]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = z * (↑(algebraMap R S) ↑(r, m).snd * ↑(↑(toInvSubmonoid M S) m))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) = mk' S 1 x
[PROOFSTEP]
rw [← (IsLocalization.map_units S x).mul_left_inj]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) * ↑(algebraMap R S) ↑x = mk' S 1 x * ↑(algebraMap R S) ↑x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x
[PROOFSTEP]
simp_rw [← toInvSubmonoid_eq_mk']
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, ↑(↑(toInvSubmonoid M S) m) = x
[PROOFSTEP]
exact
  ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩, fun h =>
    h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submodule.span R ↑(invSubmonoid M S) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
rintro x -
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩
[GOAL]
case intro.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_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
⊢ r • ↑(↑(toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
⊢ Algebra.FiniteType R S
[PROOFSTEP]
have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
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
[PROOFSTEP]
rw [Monoid.fg_iff_submonoid_fg] at this 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Submonoid.FG (invSubmonoid M S)
⊢ Algebra.FiniteType R S
[PROOFSTEP]
rcases this with ⟨s, hs⟩
[GOAL]
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_3
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
[PROOFSTEP]
refine' ⟨⟨s, _⟩⟩
[GOAL]
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_3
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 = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
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_3
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
[PROOFSTEP]
rintro x -
[GOAL]
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_3
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
[PROOFSTEP]
change x ∈ (Subalgebra.toSubmodule (Algebra.adjoin R _ : Subalgebra R S) : Set S)
[GOAL]
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_3
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))
[PROOFSTEP]
rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]
[GOAL]
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_3
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 ∈ ↑⊤
[PROOFSTEP]
trivial
