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

Proof state:
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
x : S
hx : x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r))
⊢ x ∈ ↑(Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)))

Tactic:
apply Algebra.subset_adjoin

Result:
case refine_1.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
x : S
hx : x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r))
⊢ x ∈ (⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

Proof state:
⊢ OfLocalizationSpanTarget @FiniteType

Tactic:
rw [ofLocalizationSpanTarget_iff_finite]

Result:
⊢ OfLocalizationFiniteSpanTarget @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
⊢ ∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ Algebra.adjoin R ↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l) l.support)

Tactic:
intro r

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

Tactic:
convert H r

Result:
case h.e'_5.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
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑r)).comp f).toAlgebra

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

Tactic:
rw [show ∀ A : Set S, (∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔
  (∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A) by
  { exact fun _ => by simp [Submonoid.mem_powers_iff] }]

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
r : ↑↑s
⊢ ∃ m, ↑m • x ∈ Algebra.adjoin R ((⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑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:
intro r

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

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

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case h.e'_5.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
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑r)).comp f).toAlgebra

Tactic:
ext

Result:
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
⊢ (let_fun I := OreLocalization.instAlgebra;
    r✝ • x✝) =
    r✝ • x✝

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 }), Algebra.FiniteType R (Localization.Away ↑r)
⊢ f.FiniteType

Tactic:
replace H := fun r => (H r).1

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
H : ∀ (r : { x // x ∈ s }), ⊤.FG
⊢ f.FiniteType