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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
⊢ y ∈ spanSingleton S x * I → ∃ y', y' ∈ I ∧ y = x * y'

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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
⊢ (∃ y', y' ∈ I ∧ y = x * y') → y ∈ spanSingleton S x * I
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
⊢ y ∈ spanSingleton S x * I ↔ ∃ y', y' ∈ I ∧ y = x * y'
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∃ y', y' ∈ I ∧ y = x * y'
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
⊢ y ∈ spanSingleton S x * I → ∃ y', y' ∈ I ∧ y = x * y'
intro h
case mp.refine_1
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∀ (i : P), i ∈ spanSingleton S x → ∀ (j : P), j ∈ I → ∃ y', y' ∈ I ∧ i * j = x * y'

case mp.refine_2
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∀ (x_1 y : P), (∃ y', y' ∈ I ∧ x_1 = x * y') → (∃ y', y' ∈ I ∧ y = x * y') → ∃ y', y' ∈ I ∧ x_1 + y = x * y'
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∃ y', y' ∈ I ∧ y = x * y'
refine FractionalIdeal.mul_induction_on h ?_ ?_
case mp.refine_1
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1, y'_1 ∈ I ∧ x' * y' = x * y'_1
case mp.refine_1
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∀ (i : P), i ∈ spanSingleton S x → ∀ (j : P), j ∈ I → ∃ y', y' ∈ I ∧ i * j = x * y'
intro x' hx' y' hy'
case mp.refine_1.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ ∃ y'_1, y'_1 ∈ I ∧ x' * y' = x * y'_1
case mp.refine_1
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1, y'_1 ∈ I ∧ x' * y' = x * y'_1
obtain ⟨a, ha⟩ := (mem_spanSingleton S).mp hx'
case mp.refine_1.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ x' * y' = x * a • y'
case mp.refine_1.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ ∃ y'_1, y'_1 ∈ I ∧ x' * y' = x * y'_1
use a • y', Submodule.smul_mem (I : Submodule R P) a hy'
no goals
case mp.refine_1.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : x' ∈ spanSingleton S x
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ x' * y' = x * a • y'
rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
case mp.refine_2.intro.intro.intro.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y✝ : P
I : FractionalIdeal S P
h : y✝ ∈ spanSingleton S x * I
y : P
hy : y ∈ I
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1, y'_1 ∈ I ∧ x * y + x * y' = x * y'_1
case mp.refine_2
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∀ (x_1 y : P), (∃ y', y' ∈ I ∧ x_1 = x * y') → (∃ y', y' ∈ I ∧ y = x * y') → ∃ y', y' ∈ I ∧ x_1 + y = x * y'
rintro _ _ ⟨y, hy, rfl⟩ ⟨y', hy', rfl⟩
no goals
case mp.refine_2.intro.intro.intro.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y✝ : P
I : FractionalIdeal S P
h : y✝ ∈ spanSingleton S x * I
y : P
hy : y ∈ I
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1, y'_1 ∈ I ∧ x * y + x * y' = x * y'_1
exact ⟨y + y', Submodule.add_mem (I : Submodule R P) hy hy', (mul_add _ _ _).symm⟩
case mpr.intro.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
I : FractionalIdeal S P
y' : P
hy' : y' ∈ I
⊢ x * y' ∈ spanSingleton S x * I
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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y : P
I : FractionalIdeal S P
⊢ (∃ y', y' ∈ I ∧ y = x * y') → y ∈ spanSingleton S x * I
rintro ⟨y', hy', rfl⟩
no goals
case mpr.intro.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.1449884
inst✝³ : CommRing R₁
K : Type ?u.1449890
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : P
I : FractionalIdeal S P
y' : P
hy' : y' ∈ I
⊢ x * y' ∈ spanSingleton S x * I
exact mul_mem_mul ((mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩) hy'