-- Mathlib/RingTheory/RingHom/Finite.lean
theorem multiple_mem_span_of_mem_localization_span
    {N : Type*} [AddCommMonoid N] [Module R N] [Module R' N]
    [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N)
    (hx : x ∈ Submodule.span R' s) : ∃ (t : M), t • x ∈ Submodule.span R s

Proof state:
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
⊢ ∃ t, t • x ∈ Submodule.span R s

Tactic:
obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx

Result:
case intro.intro
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R s

Proof state:
case intro.intro.intro
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
s : Set N
x : N
hx : x ∈ Submodule.span R' s
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
t : ↥M
ht : t • x ∈ Submodule.span R ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R s

Tactic:
exact ⟨t, Submodule.span_mono hss' ht⟩

Result:
no goals

Proof state:
case insert
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
x : N
hs' : x ∈ Submodule.span R' ↑(insert a s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(insert a s)

Tactic:
simp only [Finset.coe_insert, Finset.image_insert, Finset.coe_image, Subtype.coe_mk,
  Submodule.mem_span_insert] at hs' ⊢

Result:
case insert
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
x : N
hs' : ∃ a_1, ∃ z ∈ Submodule.span R' ↑s, x = a_1 • a + z
⊢ ∃ t a_1, ∃ z ∈ Submodule.span R ↑s, t • x = a_1 • a + z

Proof state:
case h
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
x : N
hs' : x ∈ Submodule.span R' ↑∅
⊢ 1 • x ∈ Submodule.span R ↑∅

Tactic:
simpa using hs'

Result:
no goals

Proof state:
case insert.intro.intro.intro.intro.mk
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
y' : R
s' : ↥M
e✝ : y * (algebraMap R R') ↑(y', s').2 = (algebraMap R R') (y', s').1
e : (y * (algebraMap R R') ↑(y', s').2) • a = (algebraMap R R') (y', s').1 • a
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Tactic:
simp only [algebraMap_smul] at e

Result:
case insert.intro.intro.intro.intro.mk
R : Type u
inst✝⁷ : CommRing R
M : Submonoid R
R' : Type u
inst✝⁶ : CommRing R'
inst✝⁵ : Algebra R R'
N : Type u_1
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
y' : R
s' : ↥M
e✝ : y * (algebraMap R R') ↑(y', s').2 = (algebraMap R R') (y', s').1
e : (y * (algebraMap R R') ↑s') • a = y' • a
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1