-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (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 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), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
We : FiniteType R S
We₁ : ∀ (hfintype : FiniteType R S), FinitePresentation R S
We₂ : FiniteType R S
We₃ We₄ : ∀ (hfintype : FiniteType R S), FinitePresentation R S
We₅ :
  ∀ (hfintype : FiniteType R S) (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
    (hf :
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑f : (a : MvPolynomial (Fin n) R) → S)),
    FinitePresentation R S
We₆ :
  ∀ (hfintype : FiniteType R S) (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
    (hf :
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑f : (a : MvPolynomial (Fin n) 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)),
    FinitePresentation R S
We₇ :
  ∀ (hfintype : FiniteType R S) (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
    (hf :
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑f : (a : MvPolynomial (Fin n) 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))
    (g' : (g : ↥s) → MvPolynomial (Fin n) R)
    (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)), FinitePresentation R S
We₈ We₉ We₁₀ :
  ∀ (hfintype : FiniteType R S) (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
    (hf :
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
        (⇑f : (a : MvPolynomial (Fin n) 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))
    (g' : (g : ↥s) → MvPolynomial (Fin n) R)
    (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S))
    (h' : (g : ↥s) → MvPolynomial (Fin n) R)
    (hh' :
      ∀ (g : ↥s),
        Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
          ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)),
    FinitePresentation R S
⊢ FinitePresentation R S
have We₁₁ : ∀ (hfintype : FiniteType R S) (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S)
  (hf :
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S)
      (⇑f : (a : MvPolynomial (Fin n) 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))
  (g' : (g : ↥s) → MvPolynomial (Fin n) R) (hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S))
  (h' : (g : ↥s) → MvPolynomial (Fin n) R)
  (hh' :
    ∀ (g : ↥s),
      Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
        ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)),
  let I : Ideal (MvPolynomial (Fin n) R) :=
    Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1};
  ∀ (hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)),
    FinitePresentation R S
Tactic: classical
  /-
  We already know that `S` is of finite type over `R`, so we have a surjection
  `MvPolynomial (Fin n) R →ₐ[R] S`. To reason about the kernel, we want to check it on the stalks
  of preimages of `s`. But the preimages do not necessarily span `MvPolynomial (Fin n) R`, so
  we quotient out by an ideal and apply `finitePresentation_ofLocalizationSpanTarget_aux`.
  -/
  have hfintype : Algebra.FiniteType R S := by
    apply Algebra.FiniteType.of_span_eq_top_target s hs
    intro x hx
    have := h ⟨x, hx⟩
    infer_instance
  obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp hfintype
  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)
  choose g' hg' using (fun g : s ↦ hf g)
  choose h' hh' using (fun g : s ↦ hf (l g))
  let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span { ∑ g : s, g' g * h' g - 1 }
  let A := MvPolynomial (Fin n) R ⧸ I
  have hfI : ∀ a ∈ I, f a = 0 := by
    intro p hp
    simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
    obtain ⟨q, rfl⟩ := hp
    simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
    rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
    · rw [← hl]
      simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]
    · rintro a -
      simp
  let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
  have hf' : Function.Surjective f' :=
    Ideal.Quotient.lift_surjective_of_surjective I hfI hf
  let t : Finset A := Finset.image (fun g ↦ g' g) Finset.univ
  have ht : Ideal.span (t : Set A) = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) := by
      apply eq_of_sub_eq_zero
      rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
      apply Ideal.subset_span
      simp
    simp_rw [← this, Finset.univ_eq_attach, map_sum, map_mul]
    refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)
    simp [t]
  have : Algebra.FinitePresentation R A := by
    apply Algebra.FinitePresentation.quotient
    simp only [Finset.univ_eq_attach, I]
    exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by simp⟩
  have Ht (g : t) : Algebra.FinitePresentation R (Localization.Away (f' g)) := by
    have : ∃ (a : S) (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = g.val := by
      obtain ⟨g, hg⟩ := g
      convert! hg
      simp [A, t]
    obtain ⟨r, hr, hrr⟩ := this
    simp only [f']
    rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
    simp_rw +instances [RingHom.coe_coe]
    rw [hg']
    apply h
  exact of_span_eq_top_target_aux f' hf' t ht Ht