-- Mathlib/RingTheory/Localization/Submodule.lean
theorem mem_span_map {x : S} {a : Set R} :
    x ∈ Ideal.span (algebraMap R S '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z : M, x = mk' S y z

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
rw [← coeSubmodule_span]

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ coeSubmodule S (Ideal.span a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z) → ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Proof state:
case mpr.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ x = mk' S 1 z • (algebraMap R S) y

Tactic:
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
refine (mem_span_iff M).trans ?_

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Proof state:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z) → ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Tactic:
rintro ⟨y, hy, z, hz⟩

Result:
case mpr.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Proof state:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
⊢ (∃ y ∈ coeSubmodule S (Ideal.span a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩, z, hz⟩

Result:
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Proof state:
case mpr.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Tactic:
refine ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, ?_⟩

Result:
case mpr.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ x = mk' S 1 z • (algebraMap R S) y

Proof state:
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ x = mk' S y z

Tactic:
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
refine ⟨y, hy, z, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ x = mk' S y z