-- Module: Mathlib.RingTheory.GradedAlgebra.FiniteType
Goal:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing S
inst_3 : SetLike σ S
inst_4 : AddSubgroupClass σ S
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
inst_6 : Algebra.FiniteType (↥(𝒜 0)) S
obtain :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    ∃ (s : Finset S),
      Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
obtain₁ obtain₂ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    ∃ (s : Finset S),
      Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i
obtain₃ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    let ι₀ :=
      (x : ↥F) ×
        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)));
    let x : (i : ι₀) → S := fun (i : ι₀) ↦
      (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                  (↑(i.fst (β := fun (x : ↥F) ↦
                        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                    S) :
                DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            (↑(i.snd (β := fun (x : ↥F) ↦
                  ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                      ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
              ι)) :
        S);
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) ⊤
obtain₄ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    let ι₀ :=
      (x : ↥F) ×
        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)));
    let x : (i : ι₀) → S := fun (i : ι₀) ↦
      (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                  (↑(i.fst (β := fun (x : ↥F) ↦
                        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                    S) :
                DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            (↑(i.snd (β := fun (x : ↥F) ↦
                  ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                      ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
              ι)) :
        S);
    (↑F : Set S) ⊆ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
obtain₅ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    let ι₀ :=
      (x : ↥F) ×
        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)));
    let x : (i : ι₀) → S := fun (i : ι₀) ↦
      (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                  (↑(i.fst (β := fun (x : ↥F) ↦
                        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                    S) :
                DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            (↑(i.snd (β := fun (x : ↥F) ↦
                  ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                      ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
              ι)) :
        S);
    ∀ ⦃s : S⦄ (hs : s ∈ (↑F : Set S)), s ∈ (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
obtain₆ :
  ∀ (F : Finset S) (hF : Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑F : Set S)) ⊤),
    let ι₀ :=
      (x : ↥F) ×
        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S)));
    let x : (i : ι₀) → S := fun (i : ι₀) ↦
      (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i))
                  (↑(i.fst (β := fun (x : ↥F) ↦
                        ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                            ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
                    S) :
                DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
              (a : ι) → ↥(𝒜 a))
            (↑(i.snd (β := fun (x : ↥F) ↦
                  ↥(DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
                      ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) (↑x : S))))) :
              ι)) :
        S);
    ∀ ⦃s : S⦄ (hs : s ∈ (↑F : Set S)),
      ∑
          i ∈
            DFinsupp.support (β := fun (i : ι) ↦ ↥(𝒜 i))
              ((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s),
          (↑((((DirectSum.decompose 𝒜 : (a : S) → DirectSum ι fun (i : ι) ↦ ↥(𝒜 i)) s :
                    DirectSum.{u_3, u_1} ι fun (i : ι) ↦ ↥(𝒜 i)) :
                  (a : ι) → ↥(𝒜 a))
                i) :
            S) ∈
        (↑(Algebra.adjoin ↥(𝒜 0) (↑(Finset.image x Finset.univ) : Set S)) : Set S)
⊢ ∃ (s : Finset S),
    Eq (α := Subalgebra (↥(𝒜 0)) S) (Algebra.adjoin ↥(𝒜 0) (↑s : Set S)) ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
classical
  obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
  let ι₀ := Σ (x : F), (DirectSum.decompose 𝒜 x.1).support
  let x (i : ι₀) : S := ((DirectSum.decompose 𝒜) i.1 i.2).1
  refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
  rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
  intro s hs
  rw [← DirectSum.sum_support_decompose 𝒜 s]
  exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)

Premises used: Algebra.subset_adjoin, Algebra.adjoin_le_iff, top_le_iff, Algebra.FiniteType.out, sum_mem