-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem coeIdeal_span_singleton (x : R) :
    (↑(Ideal.span {x} : Ideal R) : FractionalIdeal S P) = spanSingleton S (algebraMap R P x)

Proof state:
case a.mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y

Tactic:
rintro ⟨y', rfl⟩

Result:
case a.mpr.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
⊢ ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y' • (algebraMap R P) x

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ x' • (algebraMap R P) x = (algebraMap R P) (x' • x)

Tactic:
rw [smul_eq_mul, RingHom.map_mul, Algebra.smul_def]

Result:
no goals

Proof state:
case a.mp.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ ∃ z, z • (algebraMap R P) x = (algebraMap R P) (x' • x)

Tactic:
use x'

Result:
case h
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ x' • (algebraMap R P) x = (algebraMap R P) (x' • x)

Proof state:
case a.mpr.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
⊢ (algebraMap R P) (y' * x) = y' • (algebraMap R P) x

Tactic:
rw [RingHom.map_mul, Algebra.smul_def]

Result:
no goals

Proof state:
case a.mpr.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
⊢ ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y' • (algebraMap R P) x

Tactic:
refine ⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', rfl⟩, ?_⟩

Result:
case a.mpr.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
⊢ (algebraMap R P) (y' * x) = y' • (algebraMap R P) x

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S ((algebraMap R P) x)

Tactic:
refine (mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) ↔ ∃ z, z • (algebraMap R P) x = y

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
⊢ ↑(Ideal.span {x}) = spanSingleton S ((algebraMap R P) x)

Tactic:
ext y

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ spanSingleton S ((algebraMap R P) x)

Proof state:
case a.mp.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
hy' : y' ∈ Ideal.span {x}
⊢ ∃ z, z • (algebraMap R P) x = (algebraMap R P) y'

Tactic:
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'

Result:
case a.mp.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x x' : R
hy' : x' • x ∈ Ideal.span {x}
⊢ ∃ z, z • (algebraMap R P) x = (algebraMap R P) (x' • x)

Proof state:
case a.mp
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) → ∃ z, z • (algebraMap R P) x = y

Tactic:
rintro ⟨y', hy', rfl⟩

Result:
case a.mp.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y' : R
hy' : y' ∈ Ideal.span {x}
⊢ ∃ z, z • (algebraMap R P) x = (algebraMap R P) y'

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) ↔ ∃ z, z • (algebraMap R P) x = y

Tactic:
constructor

Result:
case a.mp
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y) → ∃ z, z • (algebraMap R P) x = y

case a.mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : R
y : P
⊢ (∃ z, z • (algebraMap R P) x = y) → ∃ x' ∈ Ideal.span {x}, (algebraMap R P) x' = y