case pos
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ I * (1 / I) ≤ 1

case neg
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ I * (1 / I) ≤ 1
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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
⊢ I * (1 / I) ≤ 1
by_cases hI : I = 0
case pos
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ 0 ≤ 1
case pos
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ I * (1 / I) ≤ 1
rw [hI, div_zero, MulZeroClass.mul_zero]
no goals
case pos
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ 0 ≤ 1
exact zero_le 1
case neg
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ ↑I * (1 / ↑I) ≤ 1
case neg
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ I * (1 / I) ≤ 1
rw [← coe_le_coe, coe_mul, coe_div hI, coe_one]
no goals
case neg
R : Type ?u.1197189
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1197396
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 = 0
⊢ ↑I * (1 / ↑I) ≤ 1
apply Submodule.mul_one_div_le_one