-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set R
hs_1 : Eq (α := Ideal R) (Ideal.span s_1) ⊤
s : Finset R
h₁ : (↑s : Set R) ⊆ s_1
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away (↑i : R)) (Localization.Away (↑i : R) ⊗[R] S)
letI letI₁ letI₂ : FiniteType R S
letI₃ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    FiniteType R S
out :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
out₁ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (H : ∀ (r : ↥s), Subalgebra.FG (R := Localization.Away (↑r : R)) (A := Localization.Away (↑r : R) ⊗[R] S) ⊤),
    Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
out₂ out₃ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
h₂ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    Eq (α := Subalgebra R S) (adjoin R (↑(s.attach.biUnion sf) : Set S)) ⊤
h₃ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    Eq.{u_2 + 1} (α := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) ⊤
h₄ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    ∀ (x : S), Membership.mem (γ := Subalgebra R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) x
h₅ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    ∀ (x : S) (t : Set S),
      Membership.mem (γ := Set (Set S))
          (Set.range fun (t : Subsemiring S) ↦
            ⋂ (_ :
              Membership.mem (γ := Set (Subsemiring S))
                {S_1 : Subsemiring S |
                  Set.range.{u_2, u_1 + 1} (ι := R) (⇑(algebraMap R S) : (a : R) → S) ∪
                      sSup
                        (Set.image (α := Subalgebra R S) SetLike.coe
                          (Set.range fun (x : ↥s) ↦ adjoin R (↑(sf x) : Set S))) ⊆
                    (↑S_1 : Set S)}
                t),
              (↑t : Set S))
          t →
        x ∈ t
letI₄ letI₅ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    ∀ (x : S) (t : Set S) (r : (↑(↑s : Set R) : Type u_1)),
      ∃ (n : ℕ),
        Membership.mem (γ := Submodule R S)
          ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
            Submodule R S)
          ((↑r : R) ^ n • x)
letI₆ :
  let f : R →+* S := algebraMap R S;
  ∀
    (this :
      (r : ↥s) →
        Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
    (s₂ :
      ∀ (r : ↥s),
        Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
    let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
      IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
    ∀ (x : S) (t : Set S) (r : (↑(↑s : Set R) : Type u_1)) (n₁ : ℕ)
      (hn₁ :
        Membership.mem (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
          (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
          (HSMul.hSMul (β := Localization.Away (↑r : R) ⊗[R] S)
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
              ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯)
            ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S) x :
              Localization.Away (↑r : R) ⊗[R] S))),
      ∃ (n : ℕ),
        Membership.mem (γ := Submodule R S)
          ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
            Submodule R S)
          ((↑r : R) ^ n • x)
⊢ FiniteType R S
have letI₇ : let f : R →+* S := algebraMap R S;
∀
  (this :
    (r : ↥s) →
      Algebra.{u_1, u_2} (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
  (s₁ : (r : ↥s) → Finset (Localization.Away (↑r : R) ⊗[R] S))
  (s₂ :
    ∀ (r : ↥s),
      Eq (α := Subalgebra (Localization.Away (↑r : R)) (Localization.Away (↑r : R) ⊗[R] S))
        (adjoin (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S))) ⊤),
  let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
    IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
  ∀ (x : S) (t : Set S) (r : (↑(↑s : Set R) : Type u_1)) (n₁ : ℕ)
    (hn₁ :
      Membership.mem (α := Localization.Away (↑r : R) ⊗[R] S) (γ := Subalgebra R (Localization.Away (↑r : R) ⊗[R] S))
        (adjoin R (↑(s₁ r) : Set (Localization.Away (↑r : R) ⊗[R] S)))
        ((algebraMap S (Localization.Away (↑r : R) ⊗[R] S) : (a : S) → Localization.Away (↑r : R) ⊗[R] S)
            (HMul.hMul (α := S)
              ((algebraMap R S : (a : R) → S)
                  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) sorry) :
                    R) :
                S)
              x) :
          Localization.Away (↑r : R) ⊗[R] S)),
    ∃ (n : ℕ),
      Membership.mem (γ := Submodule R S)
        ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (⨆ (x : ↥s), adjoin R (↑(sf x) : Set S)) :
          Submodule R S)
        ((↑r : R) ^ n • x)
Tactic: classical
  letI := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra
  set f := algebraMap R S
  constructor
  replace H := fun r => (h r).1
  choose s₁ s₂ using H
  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
  use s.attach.biUnion sf
  convert! (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
  rw [eq_top_iff]
  rintro x -
  apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
    _ hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
      (algebraMap S _ x) (by rw [s₂ r]; trivial)
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁
  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
  simp_rw [Submonoid.map_powers] at hn₂
  use n₂ + n₁
  exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂