-- Mathlib/RingTheory/Localization/Submodule.lean
theorem mem_span_iff {N : Type*} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
    {x : N} {a : Set N} :
    x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z : M, x = mk' S 1 z • y

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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ x = mk' S 1 1 • x

Tactic:
rw [mk'_one, map_one, one_smul]

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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ 0 = mk' S 1 1 • 0

Tactic:
rw [mk'_one, map_one, one_smul]

Result:
no goals

Proof state:
case mp.refine_4.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a✝ : Set N
h : x ∈ Submodule.span S a✝
a : S
y : N
hy : y ∈ Submodule.span R a✝
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a✝
⊢ ∃ y_1 ∈ Submodule.span R a✝, ∃ z_1, a • mk' S 1 z • y = mk' S 1 z_1 • y_1

Tactic:
obtain ⟨y', z', rfl⟩ := mk'_surjective M a

Result:
case mp.refine_4.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ ∃ y_1 ∈ Submodule.span R a, ∃ z_1, mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1

Proof state:
case mp.refine_1
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ x ∈ a, ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Tactic:
rintro x hx

Result:
case mp.refine_1
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x✝ : N
a : Set N
h : x✝ ∈ Submodule.span S a
x : N
hx : x ∈ a
⊢ ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Proof state:
case mp.refine_3.intro.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • (↑z' • y + ↑z • y')

Tactic:
rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ←
  IsScalarTower.algebraMap_smul S (z' : R), smul_smul, smul_smul]

Result:
case mp.refine_3.intro.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y + (mk' S 1 (z * z') * (algebraMap R S) ↑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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a → ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Tactic:
intro h

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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Proof state:
case mp.refine_3.intro.intro.intro.intro.intro.intro.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y = (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y

Tactic:
rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]

Result:
no goals

Proof state:
case mp.refine_4
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
⊢ ∀ (a_1 : S),
    ∀ x ∈ Submodule.span S a,
      (∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Submodule.span R a, ∃ z, a_1 • x = mk' S 1 z • y

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

Result:
case mp.refine_4.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a✝ : Set N
h : x ∈ Submodule.span S a✝
a : S
y : N
hy : y ∈ Submodule.span R a✝
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a✝
⊢ ∃ y_1 ∈ Submodule.span R a✝, ∃ z_1, a • mk' S 1 z • y = mk' S 1 z_1 • y_1

Proof state:
case mp.refine_4.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ ∃ y_1 ∈ Submodule.span R a, ∃ z_1, mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1

Tactic:
refine ⟨y' • y, Submodule.smul_mem _ _ hy, z' * z, ?_⟩

Result:
case mp.refine_4.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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y