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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J) ↔ ∀ (z : P), z ∈ I → x * z ∈ 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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ spanSingleton S x * I ≤ J ↔ ∀ (z : P), z ∈ I → x * z ∈ J
simp only [mul_le, mem_singleton_mul, mem_spanSingleton]
case mp
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J) → ∀ (z : P), z ∈ I → x * z ∈ J

case mpr
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (z : P), z ∈ I → x * z ∈ J) → ∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ 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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J) ↔ ∀ (z : P), z ∈ I → x * z ∈ J
constructor
case mp
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J
zI : P
hzI : zI ∈ I
⊢ x * zI ∈ J
case mp
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J) → ∀ (z : P), z ∈ I → x * z ∈ J
intro h zI hzI
no goals
case mp
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J
zI : P
hzI : zI ∈ I
⊢ x * zI ∈ J
exact h x ⟨1, one_smul _ _⟩ zI hzI
case mpr.intro
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (z : P), z ∈ I → x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • x * zI ∈ J
case mpr
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ (z : P), z ∈ I → x * z ∈ J) → ∀ (i : P), (∃ z, z • x = i) → ∀ (j : P), j ∈ I → i * j ∈ J
rintro h _ ⟨z, rfl⟩ zI hzI
case mpr.intro
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (z : P), z ∈ I → x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J
case mpr.intro
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (z : P), z ∈ I → x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • x * zI ∈ J
rw [Algebra.smul_mul_assoc]
no goals
case mpr.intro
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
R₁ : Type ?u.1734695
inst✝⁴ : CommRing R₁
K : Type ?u.1734701
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
h : ∀ (z : P), z ∈ I → x * z ∈ J
z : R
zI : P
hzI : zI ∈ I
⊢ z • (x * zI) ∈ J
exact Submodule.smul_mem J.1 _ (h zI hzI)