-- 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:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ (t * s') • (y • a + z) = (↑t * y') • a + ↑s' • t • z

Tactic:
rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]

Result:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ t • s' • y • a + s' • t • z = ↑t • (↑s' • y) • a + ↑s' • t • z

Proof state:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ t • s' • y • a + s' • t • z = ↑t • (↑s' • y) • a + ↑s' • t • z

Tactic:
simp

Result:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ t • s' • y • a + s' • t • z = ↑t • ↑s' • y • a + ↑s' • t • z

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✝
a✝ : ∀ 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:
rename_i a s _ 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' : x ∈ Submodule.span R' ↑(insert a s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(insert a s)

Proof state:
case insert.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'
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
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Tactic:
rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, 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
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Proof state:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Tactic:
refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩

Result:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ (t * s') • (y • a + z) = (↑t * y') • a + ↑s' • t • z

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') ↑s') • a = y' • a
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Tactic:
rcases hs _ hz with ⟨t, ht⟩

Result:
case insert.intro.intro.intro.intro.mk.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'
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 : ↥M
ht : t • z ∈ Submodule.span R ↑s
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1