case pos
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)

case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
⊢ I ≤ I * (1 / I)
by_cases hI_nz : I = 0
no goals
case pos
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)
rw [hI_nz, div_zero, MulZeroClass.mul_zero]
case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)
rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]
case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
rw [← coe_le_coe, coe_one] at hI
no goals
case neg
R : Type ?u.1202895
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1203102
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
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)
exact Submodule.le_self_mul_one_div hI