-- Mathlib/RingTheory/RingHom/Finite.lean
theorem IsLocalization.smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebra R S']
    [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S')
    (hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) :
    ∃ m : M, m • x ∈
      Submodule.span R
        (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S)

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
let g : S →ₐ[R] S' :=
  AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one]

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Proof state:
case intro.intro.intro.intro.intro.mk.intro.intro
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = g (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M)

Result:
case h
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = g (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ (⟨a, ha₁⟩ * ⟨y', hy'⟩) • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Proof state:
case intro.intro
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx : y' • (algebraMap S S') x ∈ Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
erw [← _root_.map_smul g, ← Submodule.map_span (g : S →ₗ[R] S')] at hx

Result:
case intro.intro
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx : g (y' • x) ∈ Submodule.map (↑g) (Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Proof state:
case h.e'_3
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = g (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ a • x' = ↑⟨(algebraMap R S) a, ⋯⟩ * x'

Tactic:
exact Algebra.smul_def _ _

Result:
no goals

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
have hx₁ : (y : S) • (s : Set S') = g '' _ :=
  (IsLocalization.finsetIntegerMultiple_image _ s).symm

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
M : Submonoid R
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)