-- 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
⊢ ↑r ∈ ↑(Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support))).toSubmonoid

Tactic:
apply Algebra.subset_adjoin

Result:
case refine_2.a
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 ∈ (⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

Proof state:
case refine_2.a
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 ∈ (⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

Tactic:
exact Or.inl (Or.inr r.2)

Result:
no goals

Proof state:
case a
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✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(s.attach.biUnion sf) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

Tactic:
exact Or.inl (Or.inr hx)

Result:
no goals

Proof state:
case h
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)
⊢ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support) = ⊤

Tactic:
rw [eq_top_iff]

Result:
case h
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)
⊢ ⊤ ≤ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Proof state:
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)

Tactic:
rw [ht]

Result:
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 ∈ ⊤

Proof state:
case a
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✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
rw [Finset.coe_union, Finset.coe_union]

Result:
case a
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✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(s.attach.biUnion sf) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

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
this : Algebra R S := f.toAlgebra
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑r)

Tactic:
simp_rw [RingHom.FiniteType] at H

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 }), Algebra.FiniteType R (Localization.Away ↑r)
this : Algebra R S := f.toAlgebra
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑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
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✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support))

Tactic:
apply Algebra.subset_adjoin

Result:
case a
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✝ x : S
hx : x ∈ ↑s
⊢ x ∈ ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)