case a
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S (↑(algebraMap R P) x)
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
⊢ ↑(Ideal.span {x}) = spanSingleton S (↑(algebraMap R P) x)
ext y
case a
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y) ↔ ∃ z, z • ↑(algebraMap R P) x = y
case a
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S (↑(algebraMap R P) x)
refine' (mem_coeIdeal S).trans (Iff.trans _ (mem_spanSingleton S).symm)
case a.mp
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y) → ∃ z, z • ↑(algebraMap R P) x = y

case a.mpr
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ z, z • ↑(algebraMap R P) x = y) → ∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y
case a
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y) ↔ ∃ z, z • ↑(algebraMap R P) x = y
constructor
case a.mp.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
hy' : y' ∈ Ideal.span {x}
⊢ ∃ z, z • ↑(algebraMap R P) x = ↑(algebraMap R P) y'
case a.mp
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y) → ∃ z, z • ↑(algebraMap R P) x = y
rintro ⟨y', hy', rfl⟩
case a.mp.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ ∃ z, z • ↑(algebraMap R P) x = ↑(algebraMap R P) (x' • x)
case a.mp.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
hy' : y' ∈ Ideal.span {x}
⊢ ∃ z, z • ↑(algebraMap R P) x = ↑(algebraMap R P) y'
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'
case a.mp.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ x' • ↑(algebraMap R P) x = ↑(algebraMap R P) (x' • x)
case a.mp.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ ∃ z, z • ↑(algebraMap R P) x = ↑(algebraMap R P) (x' • x)
use x'
no goals
case a.mp.intro.intro.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ x' • ↑(algebraMap R P) x = ↑(algebraMap R P) (x' • x)
rw [smul_eq_mul, RingHom.map_mul, Algebra.smul_def]
case a.mpr.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
⊢ ∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y' • ↑(algebraMap R P) x
case a.mpr
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R
y : P
⊢ (∃ z, z • ↑(algebraMap R P) x = y) → ∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y
rintro ⟨y', rfl⟩
case a.mpr.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
⊢ ↑(algebraMap R P) (y' * x) = y' • ↑(algebraMap R P) x
case a.mpr.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
⊢ ∃ x', x' ∈ Ideal.span {x} ∧ ↑(algebraMap R P) x' = y' • ↑(algebraMap R P) x
refine' ⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', rfl⟩, _⟩
no goals
case a.mpr.intro
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1339818
inst✝³ : CommRing R₁
K : Type ?u.1339824
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x y' : R
⊢ ↑(algebraMap R P) (y' * x) = y' • ↑(algebraMap R P) x
rw [RingHom.map_mul, Algebra.smul_def]