-- 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
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

Tactic:
rcases hs' with ⟨y, z, hz, rfl⟩

Result:
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

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
s' : Finset N
hss' : ↑s' ⊆ s
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

Tactic:
clear hx hss' s

Result:
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
s' : Finset N
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

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

Tactic:
apply congrArg (fun x ↦ x • a) 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') ↑(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

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'
x : N
s' : Finset N
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

Tactic:
induction s' using Finset.induction_on generalizing x

Result:
case empty
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' ↑∅
⊢ ∃ t, t • x ∈ Submodule.span R ↑∅

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✝)

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:
rfl

Result:
no goals

Proof state:
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

Tactic:
rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)

Result:
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

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 empty
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' ↑∅
⊢ ∃ t, t • x ∈ Submodule.span R ↑∅

Tactic:
use 1

Result:
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 ↑∅