-- Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FiniteType.{u_1, u_2} R (Localization.Away (↑i : S))
Suppose Suppose₁ Suppose₂ :
  ∀ (h : ∀ (r : ↥s), Subalgebra.FG.{u_1, u_2} (R := R) (A := Localization.Away (↑r : S)) ⊤), FiniteType R S
Suppose₃ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤),
    FiniteType R S
Suppose₄ Suppose₅ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    FiniteType R S
h₂ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    Eq (α := Subalgebra R S)
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
      ⊤
h₃ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    LE.le (α := Subalgebra R S) ⊤
      (adjoin R
        (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
h₄ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄,
      Membership.mem (γ := Subalgebra R S)
        (adjoin R
          (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
        x
Suppose₆ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄,
      (↑s : Set S) ⊆
        (↑(adjoin R
              (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) :
                Set S)) :
          Set S)
Suppose₇ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄ (i : (↑(↑s : Set S) : Type u_2)),
      Membership.mem (α := S) (γ := Subalgebra R S)
        (adjoin R
          (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
        ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
Suppose₈ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄ (r : (↑(↑s : Set S) : Type u_2)),
      ∃ (n : ℕ),
        Membership.mem (γ := Subalgebra R S)
          (adjoin R
            (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
          ((↑r : S) ^ n • x)
Suppose₉ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄ (i : (↑(↑s : Set S) : Type u_2)),
      Membership.mem (α := S) (γ := Subalgebra R S)
        (adjoin R
          (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
        ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) i : S)
Suppose₁₀ Suppose₁₁ :
  ∀ (t : (r : ↥s) → Finset (Localization.Away (↑r : S)))
    (ht :
      ∀ (r : ↥s),
        Eq (α := Subalgebra R (Localization.Away (↑r : S))) (adjoin R (↑(t r) : Set (Localization.Away (↑r : S)))) ⊤)
    (l : (↑(↑s : Set S) : Type u_2) →₀ S)
    (hl :
      Eq (α := S)
        ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
              (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
            l :
          S)
        (1 : S)),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers (↑x : S)) (t x);
    ∀ ⦃x : S⦄ (r : (↑(↑s : Set S) : Type u_2)),
      ∃ (n : ℕ),
        Membership.mem (γ := Subalgebra R S)
          (adjoin R
            (↑(s.attach.biUnion sf ∪ s ∪ Finset.image (⇑l : (a : (↑(↑s : Set S) : Type u_2)) → S) l.support) : Set S))
          ((↑r : S) ^ n • x)
⊢ FiniteType R S

Tactic:
classical
  -- 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`.
  replace h := fun r => (h r).1
  choose t ht using h
  obtain ⟨l, hl⟩ :=
    (Finsupp.mem_span_iff_linearCombination 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 [_root_.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

Premises used: Set.singleton_subset_iff, Finset.coe_biUnion, eq_top_iff, Finsupp.mem_span_iff_linearCombination, Algebra.subset_adjoin, Finset.coe_image, Submonoid.powers_eq_closure, SetLike.coe, Iff.mp, Or.inl, ZeroMemClass.zero_mem, OfNat.ofNat, Submonoid.closure_le, Finset.coe_union