-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
H : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
    Ideal.FG (RingHom.ker f.toRingHom) :=
  ⋯
n : ℕ :=
  H.choose (p := fun (n : ℕ) ↦
    ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
          (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
        Ideal.FG (RingHom.ker f.toRingHom))
f : MvPolynomial (Fin n) R →ₐ[R] S :=
  ⋯.choose (p :=
    fun
      (f :
        MvPolynomial
            (Fin
              (H.choose (p := fun (n : ℕ) ↦
                ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                      (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                    Ideal.FG (RingHom.ker f.toRingHom))))
            R →ₐ[R]
          S) ↦
    Function.Surjective.{u + 1, v + 1} (α :=
        MvPolynomial
          (Fin
            (H.choose (p := fun (n : ℕ) ↦
              ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                    (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                  Ideal.FG (RingHom.ker f.toRingHom))))
          R)
        (β := S) (⇑f : (a : MvPolynomial (Fin H.choose) R) → S) ∧
      Ideal.FG (RingHom.ker f.toRingHom))
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
hf' : Ideal.FG (RingHom.ker f)
H' : ∃ (n_1 : ℕ) (s : Fin n_1 → MvPolynomial (Fin n) R),
  Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
    (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f) :=
  ⋯
m : ℕ :=
  H'.choose (p := fun (n_1 : ℕ) ↦
    ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
      Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
        (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
v : Fin m → MvPolynomial (Fin n) R :=
  ⋯.choose (p :=
    fun
      (s :
        Fin
            (H'.choose (p := fun (n_1 : ℕ) ↦
              ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
                Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
                  (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))) →
          MvPolynomial (Fin n) R) ↦
    Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
      (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
hv : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range v)) (RingHom.ker f)
⊢ f = aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)
have e_f : ∀ (i : Fin n),
  Eq.{v + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
    ((aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x) : (a : MvPolynomial (Fin n) R) → S) (X i) :
      S)
Tactic: ext