-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem finiteType_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FiniteType

Proof state:
case refine_2
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ Submonoid.powers ↑r ≤
    (Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

Tactic:
rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]

Result:
case refine_2
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑r ∈ ↑(Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
⊢ l i ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
by_cases h : l i = 0

Result:
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : l i = 0
⊢ l i ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

case neg
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
h : ¬l i = 0
⊢ l i ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Proof state:
case h.e'_5.h.h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := f.toAlgebra
r : { x // x ∈ s }
e_4✝ : OreLocalization.instSemiring = CommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers ↑r) S
⊢ (algebraMap R (OreLocalization (Submonoid.powers ↑r) S)) r✝ * x✝ =
    (algebraMap R (OreLocalization (Submonoid.powers ↑r) S)) r✝ * x✝

Tactic:
rfl

Result:
no goals

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∃ m, ↑m • x ∈ Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))

Tactic:
refine IsLocalization.exists_smul_mem_of_mem_adjoin
  (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_

Result:
case refine_1
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r)) ⊆
    ↑(Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)))

case refine_2
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ Submonoid.powers ↑r ≤
    (Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

case refine_3
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ Algebra.adjoin R ↑(t r)

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
H : ∀ (r : { x // x ∈ s }), ⊤.FG
⊢ f.FiniteType

Tactic:
constructor

Result:
case out
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
H : ∀ (r : { x // x ∈ s }), ⊤.FG
⊢ ⊤.FG

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), ((algebraMap S (Localization.Away ↑r)).comp f).FiniteType
⊢ f.FiniteType

Tactic:
letI := f.toAlgebra

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), ((algebraMap S (Localization.Away ↑r)).comp f).FiniteType
this : Algebra R S := f.toAlgebra
⊢ f.FiniteType

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ ∀ (i : ↑↑s), l i ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
intro i

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f.toAlgebra
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
i : ↑↑s
⊢ l i ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)