R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.763155
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.763608
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inj : Function.Injective ↑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ FG ↑↑I
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.763155
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.763608
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inj : Function.Injective ↑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ Ideal.FG I
rw [← coeIdeal_fg S inj I]
no goals
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.763155
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.763608
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
inj : Function.Injective ↑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ FG ↑↑I
exact FractionalIdeal.fg_of_isUnit I h