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
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun x x_1 => x * x_1) I J ≤ (fun x x_1 => x * x_1) I J'
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
I : FractionalIdeal S P
⊢ Monotone ((fun x x_1 => x * x_1) I)
intro J J' h
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
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } ≤
    { val := ↑I * ↑J', property := (_ : IsFractional S (↑I * ↑J')) }
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
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun x x_1 => x * x_1) I J ≤ (fun x x_1 => x * x_1) I J'
simp only [mul_def]
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
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } ≤
    { val := ↑I * ↑J', property := (_ : IsFractional S (↑I * ↑J')) }
exact mul_le.mpr fun x hx y hy => mul_mem_mul hx (h hy)