R : Type ?u.1744445
inst✝⁵ : CommRing R
S : Submonoid R
P : Type ?u.1744652
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝² : CommRing R₁
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R₁ K
frac : IsFractionRing R₁ K
I : Submodule R₁ K
hI : I ≤ ⊥
⊢ FG I
R : Type ?u.1744445
inst✝⁵ : CommRing R
S : Submonoid R
P : Type ?u.1744652
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝² : CommRing R₁
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R₁ K
frac : IsFractionRing R₁ K
I : Submodule R₁ K
hI : I ≤ ↑0
⊢ FG I
rw [coe_zero] at hI
R : Type ?u.1744445
inst✝⁵ : CommRing R
S : Submonoid R
P : Type ?u.1744652
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝² : CommRing R₁
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R₁ K
frac : IsFractionRing R₁ K
I : Submodule R₁ K
hI : I ≤ ⊥
⊢ FG ⊥
R : Type ?u.1744445
inst✝⁵ : CommRing R
S : Submonoid R
P : Type ?u.1744652
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝² : CommRing R₁
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R₁ K
frac : IsFractionRing R₁ K
I : Submodule R₁ K
hI : I ≤ ⊥
⊢ FG I
rw [le_bot_iff.mp hI]
no goals
R : Type ?u.1744445
inst✝⁵ : CommRing R
S : Submonoid R
P : Type ?u.1744652
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝² : CommRing R₁
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R₁ K
frac : IsFractionRing R₁ K
I : Submodule R₁ K
hI : I ≤ ⊥
⊢ FG ⊥
exact fg_bot