-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple [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 ∈ Algebra.adjoin R (s : Set S')) :
    ∃ m : M, m • x ∈
      Algebra.adjoin R
        (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S)

Proof state:
case 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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e :
  ⟨(algebraMap R S) a, ⋯⟩ • x ∈
    Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
refine ⟨⟨a, ha⟩, ?_⟩

Result:
case 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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e :
  ⟨(algebraMap R S) a, ⋯⟩ • x ∈
    Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ⟨a, ha⟩ • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Proof state:
case 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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e :
  ⟨(algebraMap R S) a, ⋯⟩ • x ∈
    Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ⟨a, ha⟩ • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
simpa only [Submonoid.smul_def, algebraMap_smul] using e

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 ∈ Algebra.adjoin R ↑s
⊢ ∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
obtain ⟨⟨_, a, ha, rfl⟩, e⟩ :=
  IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _)
    Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx

Result:
case 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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
ha : a ∈ ↑M
e :
  ⟨(algebraMap R S) a, ⋯⟩ • x ∈
    Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
⊢ ∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) 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 ∈ Algebra.adjoin R ↑s
⊢ Submonoid.map (algebraMap R S) M ≤
    (Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)).toSubmonoid

Tactic:
rintro _ ⟨a, _, rfl⟩

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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
left✝ : a ∈ ↑M
⊢ (algebraMap R S) a ∈
    (Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)).toSubmonoid

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'
hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s
a : R
left✝ : a ∈ ↑M
⊢ (algebraMap R S) a ∈
    (Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)).toSubmonoid

Tactic:
exact Subalgebra.algebraMap_mem _ a

Result:
no goals