-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
rw rw₁ rw₂ : OfLocalizationFiniteSpan @Finite
rw₃ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
    (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))), f.Finite
rw₄ rw₅ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
    (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))), f.Finite
rw₆ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
    (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))),
    let this := f.toAlgebra;
    ∀
      (this :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
      f.Finite
rw₇ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
    (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
      f.Finite
fg_top :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤)
    (H : ∀ (r : ↥s), Finite (A := Localization.Away (↑r : R)) (Localization.awayMap f (↑r : R))),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
      Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
fg_top₁ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (H :
        ∀ (r : ↥s),
          Submodule.FG.{u_5, u_5} (R := Localization.Away (↑r : R)) (M :=
            Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) ⊤),
      Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
fg_top₂ fg_top₃ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      Submodule.FG.{u_5, u_5} (R := R) (M := S) ⊤
h :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      Eq (α := Submodule R S) (Submodule.span R (↑(s.attach.biUnion sf) : Set S)) ⊤
h₁ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      LE.le.{u_5} (α := Submodule R S) ⊤ (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S))
h₂ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      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 (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) x
rw₈ rw₉ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₀ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (γ := Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            (HSMul.hSMul (β := Localization.Away (M := S) ((f : (a : R) → S) (↑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 (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                    (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                  x :
                Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₁ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (γ := Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            (HSMul.hSMul (α := ↥(Submonoid.powers (↑r : R))) (β :=
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                ((↑r : R) ^ n₁) ⋯)
              ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                    (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                  x :
                Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₂ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
            Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                  (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                (HMul.hMul (α := S)
                  ((algebraMap R S : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((↑r : R) ^ n₁) ⋯) :
                        R) :
                    S)
                  x) :
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₃ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
            Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                  (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                (HMul.hMul (α := S)
                  ((algebraMap R S : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((↑r : R) ^ n₁) ⋯) :
                        R) :
                    S)
                  x) :
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R S)
            (Submodule.span R
              (↑(IsLocalization.finsetIntegerMultiple
                    (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
                Set S))
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
              HMul.hMul (α := S)
                ((algebraMap R S : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((↑r : R) ^ n₁) ⋯) :
                      R) :
                  S)
                x)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₄ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
            Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                  (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                (HMul.hMul (α := S)
                  ((algebraMap R S : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((↑r : R) ^ n₁) ⋯) :
                        R) :
                    S)
                  x) :
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R S)
            (Submodule.span R
              (↑(IsLocalization.finsetIntegerMultiple
                    (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
                Set S))
            ((↑r : R) ^ (n₂ + n₁) • x)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
rw₁₅ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
            Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                  (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                (HMul.hMul (α := S)
                  ((algebraMap R S : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((↑r : R) ^ n₁) ⋯) :
                        R) :
                    S)
                  x) :
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R S)
            (Submodule.span R
              (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)))
                      (s₁ r) :
                    Finset S) :
                Set S))
            ((↑r : R) ^ (n₂ + n₁) • x)),
        ∃ (n : ℕ),
          Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)
h₃ :
  ∀ ⦃R S : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R)
    (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤),
    let this := f.toAlgebra;
    let this_1 :
      (r : ↥s) → Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
      fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R));
    ∀
      (this_2 :
        ∀ (r : ↥s),
          IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
            (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (this_3 :
        ∀ (r : ↥s),
          IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (s₂ :
        ∀ (r : ↥s),
          Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span (Localization.Away (↑r : R))
              (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ⊤),
      let sf : (x : ↥s) → Finset S := fun (x : ↥s) ↦
        IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x);
      ∀ ⦃x : S⦄ (r : (↑(↑s : Set R) : Type u_5)) (n₁ : ℕ)
        (hn₁ :
          Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
            Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
            (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
            ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
                  (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
                (HMul.hMul (α := S)
                  ((algebraMap R S : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((↑r : R) ^ n₁) ⋯) :
                        R) :
                    S)
                  x) :
              Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
        (n₂ : ℕ)
        (hn₂ :
          Membership.mem (γ := Submodule R S)
            (Submodule.span R
              (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R)))
                      (s₁ r) :
                    Finset S) :
                Set S))
            ((↑r : R) ^ (n₂ + n₁) • x)),
        Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ (n₂ + n₁) • x)
⊢ OfLocalizationSpan @Finite

Tactic:
classical
  rw [RingHom.ofLocalizationSpan_iff_finite]
  introv R hs H
  -- We first setup the instances
  letI := f.toAlgebra
  letI := fun r : s => (Localization.awayMap f r).toAlgebra
  have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S))
      (Localization.Away (f r)) := by
    rw [Submonoid.map_powers]; exact Localization.isLocalization
  haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) :=
    fun r => IsScalarTower.of_algebraMap_eq'
      (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
  -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be
  -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of
  -- these generates `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
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`.
  -- This then follows from the fact that each `x : R` is a linear combination of the generating set
  -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the
  -- denominators of both the generating set and the coefficients.
  rintro x -
  apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
  intro r
  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x)
      (by rw [s₂ r]; trivial)
  dsimp only at hn₁
  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
    IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R))
      (Localization.Away (f 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 => Submodule.span R (sf x : Set S)) r hn₂

Premises used: eq_top_iff, Submodule.span_attach_biUnion, pow_add, smul_smul, Submonoid.smul_def, map_mul, RingHom.ofLocalizationSpan_iff_finite, Algebra.smul_def, Submonoid.map_powers, rfl