[GOAL]
⊢ StableUnderComposition @FiniteType
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : FiniteType f
hg : FiniteType g
⊢ FiniteType (comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ HoldsForLocalizationAway @FiniteType
[PROOFSTEP]
introv R _
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ FiniteType (algebraMap R S)
[PROOFSTEP]
suffices Algebra.FiniteType R S by
  rw [RingHom.FiniteType]
  convert this; ext; rw [Algebra.smul_def]; rfl
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ FiniteType (algebraMap R S)
[PROOFSTEP]
rw [RingHom.FiniteType]
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ Algebra.FiniteType R S
[PROOFSTEP]
convert this
[GOAL]
case h.e'_5
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
⊢ toAlgebra (algebraMap R S) = inst✝¹
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := toAlgebra (algebraMap R S);
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
rw [Algebra.smul_def]
[GOAL]
case h.e'_5.h
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : Algebra.FiniteType R S
r✝ : R
x✝ : S
⊢ (let_fun I := toAlgebra (algebraMap R S);
    r✝ • x✝) =
    ↑(algebraMap R S) r✝ * x✝
[PROOFSTEP]
rfl
[GOAL]
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FiniteType R S
[PROOFSTEP]
exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S
[GOAL]
⊢ OfLocalizationSpanTarget @FiniteType
[PROOFSTEP]
rw [ofLocalizationSpanTarget_iff_finite]
[GOAL]
⊢ OfLocalizationFiniteSpanTarget @FiniteType
[PROOFSTEP]
introv R hs H
[GOAL]
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 }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
⊢ FiniteType f
[PROOFSTEP]
classical
letI := f.toAlgebra
replace H : ∀ r : s, Algebra.FiniteType R (Localization.Away (r : S))
· intro r; simp_rw [RingHom.FiniteType] at H ; convert H r; ext; simp_rw [Algebra.smul_def]; rfl
replace H := fun r => (H r).1
constructor
  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
    -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
    -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
choose t ht using H
obtain ⟨l, hl⟩ :=
  (Finsupp.mem_span_iff_total S (s : Set S) 1).mp (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
use s.attach.biUnion sf ∪ s ∪ l.support.image l
rw [eq_top_iff]
  -- We need to show that every `x` falls in the subalgebra generated by those elements.
    -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
    -- the algebra for each `sᵢ` and some `nᵢ`.
rintro x -
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
· intro x hx
  apply Algebra.subset_adjoin
  rw [Finset.coe_union, Finset.coe_union]
  exact Or.inl (Or.inr hx)
· intro i
  by_cases h : l i = 0; · rw [h]; exact zero_mem _
  apply Algebra.subset_adjoin
  rw [Finset.coe_union, Finset.coe_image]
  exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
· intro r
  rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
    -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
        -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
        -- Porting note: The following `obtain` fails because Lean wants to know right away what the
        -- placeholders are, so we need to provide a little more guidance
        -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
        --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
  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]
    }]
  refine IsLocalization.exists_smul_mem_of_mem_adjoin (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
  · intro x hx
    apply Algebra.subset_adjoin
    exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
  · rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
    apply Algebra.subset_adjoin
    exact Or.inl (Or.inr r.2)
  · rw [ht]; trivial
[GOAL]
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 }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
⊢ FiniteType f
[PROOFSTEP]
letI := f.toAlgebra
[GOAL]
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 }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
⊢ FiniteType f
[PROOFSTEP]
replace H : ∀ r : s, Algebra.FiniteType R (Localization.Away (r : S))
[GOAL]
case 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 }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
⊢ ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
intro r
[GOAL]
case 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 }), FiniteType (comp (algebraMap S (Localization.Away ↑r)) f)
this : Algebra R S := toAlgebra f
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
simp_rw [RingHom.FiniteType] at H 
[GOAL]
case 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 := toAlgebra f
r : { x // x ∈ s }
⊢ Algebra.FiniteType R (Localization.Away ↑r)
[PROOFSTEP]
convert H r
[GOAL]
case h.e'_5
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 := toAlgebra f
r : { x // x ∈ s }
⊢ Localization.algebra = toAlgebra (comp (algebraMap S (Localization.Away ↑r)) f)
[PROOFSTEP]
ext
[GOAL]
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 := toAlgebra f
r : { x // x ∈ s }
r✝ : R
x✝ : Localization (Submonoid.powers ↑r)
⊢ (let_fun I := Localization.algebra;
    r✝ • x✝) =
    r✝ • x✝
[PROOFSTEP]
simp_rw [Algebra.smul_def]
[GOAL]
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 := toAlgebra f
r : { x // x ∈ s }
r✝ : R
x✝ : Localization (Submonoid.powers ↑r)
⊢ ↑(algebraMap R (Localization (Submonoid.powers ↑r))) r✝ * x✝ = r✝ • x✝
[PROOFSTEP]
rfl
[GOAL]
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 := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Algebra.FiniteType R (Localization.Away ↑r)
⊢ FiniteType f
[PROOFSTEP]
replace H := fun r => (H r).1
[GOAL]
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 := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Subalgebra.FG ⊤
⊢ FiniteType f
[PROOFSTEP]
constructor
  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
    -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
    -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
[GOAL]
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 := toAlgebra f
H : ∀ (r : { x // x ∈ s }), Subalgebra.FG ⊤
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
choose t ht using H
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
obtain ⟨l, hl⟩ :=
  (Finsupp.mem_span_iff_total S (s : Set S) 1).mp (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ 1 ∈ Ideal.span ↑s
[PROOFSTEP]
rw [hs]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case out.intro
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
[GOAL]
case out.intro
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
use s.attach.biUnion sf ∪ s ∪ l.support.image l
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
  -- We need to show that every `x` falls in the subalgebra generated by those elements.
    -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
    -- the algebra for each `sᵢ` and some `nᵢ`.
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ ⊤ ≤ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rintro x -
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ x ∈ Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
⊢ ↑s ⊆ ↑(Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support))
[PROOFSTEP]
intro x hx
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_union]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ∈ ↑(Finset.biUnion (Finset.attach s) sf) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inr hx)
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
intro i
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
by_cases h : l i = 0
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [h]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
exact zero_mem _
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
case neg.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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_image]
[GOAL]
case neg.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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ∈ ↑(Finset.biUnion (Finset.attach s) sf ∪ s) ∪ ↑l '' ↑l.support
[PROOFSTEP]
exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
intro r
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ↑(Finset.biUnion (Finset.attach s) sf ∪ s ∪ Finset.image (↑l) l.support)
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
  -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
      -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
      -- Porting note: The following `obtain` fails because Lean wants to know right away what the
      -- placeholders are, so we need to provide a little more guidance
      -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
      --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support))
[PROOFSTEP]
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]
  }]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∀ (A : Set S), (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R A) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R A
[PROOFSTEP]
{exact fun _ => by simp [Submonoid.mem_powers_iff]
}
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S S Subtype.val) l = 1
sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ ∀ (A : Set S), (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R A) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R A
[PROOFSTEP]
exact fun _ => by simp [Submonoid.mem_powers_iff]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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✝ : Set S
⊢ (∃ n, ↑r ^ n • x ∈ Algebra.adjoin R x✝) ↔ ∃ m, ↑m • x ∈ Algebra.adjoin R x✝
[PROOFSTEP]
simp [Submonoid.mem_powers_iff]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support))
[PROOFSTEP]
refine IsLocalization.exists_smul_mem_of_mem_adjoin (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)))
[PROOFSTEP]
intro x hx
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)))
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪
            ↑(Finset.image (↑l) l.support))).toSubsemiring.toSubmonoid
[PROOFSTEP]
rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪
              ↑(Finset.image (↑l) l.support))).toSubsemiring.toSubmonoid
[PROOFSTEP]
apply Algebra.subset_adjoin
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 : { x // x ∈ s }) (_ : x ∈ ↑(Finset.attach s)), ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (↑l) l.support)
[PROOFSTEP]
exact Or.inl (Or.inr r.2)
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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)
[PROOFSTEP]
rw [ht]
[GOAL]
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 := toAlgebra f
t : (r : { x // x ∈ s }) → Finset (Localization.Away ↑r)
ht : ∀ (r : { x // x ∈ s }), Algebra.adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : ↑(Finsupp.total (↑↑s) S 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 ∈ ⊤
[PROOFSTEP]
trivial
