-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
inst_7 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_8 : AtPrime.IsLiesOverAlgebra p q
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
obtain₁ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    Eq (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (↑(Finset.image
              (⇑(AlgHom.toLinearMap (IsScalarTower.toAlgHom R S (Localization.AtPrime q))) :
                (a : S) → Localization.AtPrime q)
              s) :
          Set (Localization.AtPrime q)))
      ⊤
obtain₂ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤),
    LE.le (α := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)) ⊤
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
obtain₃ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤) ⦃x : Localization.AtPrime q⦄,
    Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
      x
obtain₄ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤) (x s : S) (hsq : s ∈ q.primeCompl),
    Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
      (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
obtain₅ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤) (x s : S) (hsq : s ∈ q.primeCompl)
    (r : R) (hr : r ∉ p) (t : S) (e' : (algebraMap R S : (a : R) → S) r = s * t),
    Membership.mem (γ := Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
      (IsLocalization.mk' (Localization.AtPrime q) x (Subtype.mk (p := fun (x : S) ↦ x ∈ q.primeCompl) s hsq))
obtain₆ :
  ∀ (s : Finset S) (hs : Eq (α := Submodule R S) (Submodule.span R (↑s : Set S)) ⊤) (x s : S) (hsq : s ∈ q.primeCompl)
    (r : R) (hr : r ∉ p) (t : S) (e' : (algebraMap R S : (a : R) → S) r = s * t),
    Membership.mem (α := Localization.AtPrime q) (γ :=
      Submodule.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (Submodule.span (Localization.AtPrime p)
        (Set.range (ι := S) (⇑(algebraMap S (Localization.AtPrime q)) : (a : S) → Localization.AtPrime q)))
      ((algebraMap S (Localization.AtPrime q) : (a : S) → Localization.AtPrime q) (t * x) : Localization.AtPrime q)
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
classical
  obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := R) (M := S)
  refine ⟨s.image (IsScalarTower.toAlgHom R _ _).toLinearMap, ?_⟩
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs,
    Submodule.map_top, LinearMap.coe_range, AlgHom.coe_toLinearMap, IsScalarTower.coe_toAlgHom',
    ← top_le_iff]
  rintro x -
  obtain ⟨x, ⟨s, hsq⟩, rfl⟩ := IsLocalization.exists_mk'_eq q.primeCompl x
  obtain ⟨r, hr, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hsq
  rw [← Submodule.smul_mem_iff_of_isUnit _ (IsLocalization.map_units (M := p.primeCompl) _ ⟨r, hr⟩),
    Algebra.smul_def, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply _ S, e',
      map_mul, mul_assoc, mul_left_comm, IsLocalization.mk'_spec'_mk, ← map_mul]
  exact Submodule.subset_span ⟨_, rfl⟩

Premises used: AlgHom.coe_toLinearMap, Submodule.span_span_of_tower, Module.Finite.fg_top, IsScalarTower.coe_toAlgHom', Localization.r, Submodule.map_top, mul_assoc, Finset.coe_image, LinearMap.coe_range, mul_left_comm, map_mul, top_le_iff, IsLocalization.mk'_spec'_mk, Algebra.smul_def, Submodule.map_span, IsScalarTower.algebraMap_apply, rfl