-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem IsLocalization.exists_smul_mem_of_mem_adjoin [Algebra R S] [Algebra R S']
    [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S')
    (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A)
    (hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) :
    ∃ m : M, m • x ∈ A

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
⊢ ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑(Subalgebra.map g A)

Tactic:
exact Set.image_subset _ hA₁

Result:
no goals

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
⊢ ∃ m, m • x ∈ A

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
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
⊢ ∃ m, m • x ∈ A

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
⊢ ↑y • ↑s ⊆ ↑(Subalgebra.map g A)

Tactic:
rw [hx₁]

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
⊢ ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑(Subalgebra.map g A)

Proof state:
case intro.intro.intro.intro
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ ∃ m, m • x ∈ A

Tactic:
use a * y ^ n

Result:
case h
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ (a * y ^ n) • x ∈ A

Proof state:
case h.e'_5
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := IsLocalization.commonDenomOfFinset M s
hx₁ : ↑y • ↑s = ⇑g '' ↑(IsLocalization.finsetIntegerMultiple M s)
n : ℕ
hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A
x' : S
hx' : x' ∈ ↑A.toSubsemiring
hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)
a : ↥M
ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)
⊢ (a * y ^ n) • x = x' * ↑a

Tactic:
rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
  mul_comm]

Result:
no goals

Proof state:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
⊢ ∃ m, m • x ∈ A

Tactic:
let g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'

Result:
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
S' : Type u
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
M : Submonoid S
inst✝ : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A
hA₂ : M ≤ A.toSubmonoid
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
⊢ ∃ m, m • x ∈ A