-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
obtain :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₁ obtain₂ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₃ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom))
    (this :
      ∀ (i : Fin n),
        ∃ (a : MvPolynomial (Fin m) R),
          Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) a : A)
            ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₄ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom))
    (g : (i : Fin n) → MvPolynomial (Fin m) R)
    (hg :
      ∀ (i : Fin n),
        Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
          ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₅ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom))
    (g : (i : Fin n) → MvPolynomial (Fin m) R)
    (hg :
      ∀ (i : Fin n),
        Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
          ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
    (this :
      ∀ (i : Fin m),
        ∃ (a : MvPolynomial (Fin n) R),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) a : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₆ obtain₇ obtain₈ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom))
    (g : (i : Fin n) → MvPolynomial (Fin m) R)
    (hg :
      ∀ (i : Fin n),
        Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
          ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
    (h : (i : Fin m) → MvPolynomial (Fin n) R)
    (hh :
      ∀ (i : Fin m),
        Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
          ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
    Ideal.FG (RingHom.ker f.toRingHom)
obtain₉ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    let RXn := MvPolynomial (Fin n) R;
    let RXm := MvPolynomial (Fin m) R;
    ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
      (hg :
        ∀ (i : Fin n),
          Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
            ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
      (h : (i : Fin m) → MvPolynomial (Fin n) R)
      (hh :
        ∀ (i : Fin m),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
      let aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h;
      let g' : Fin n → RXn := fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn);
      Eq (α := Ideal (MvPolynomial (Fin n) R))
        (Ideal.span
          (↑(Finset.image g' Finset.univ ∪ Finset.image (⇑aeval_h : (a : RXm) → RXn) s) : Set (MvPolynomial (Fin n) R)))
        (RingHom.ker f.toRingHom)
obtain₁₀ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    let RXn := MvPolynomial (Fin n) R;
    let RXm := MvPolynomial (Fin m) R;
    ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
      (hg :
        ∀ (i : Fin n),
          Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
            ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
      (h : (i : Fin m) → MvPolynomial (Fin n) R)
      (hh :
        ∀ (i : Fin m),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
      let aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h;
      let g' : Fin n → RXn := fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn);
      Eq (α := Ideal (MvPolynomial (Fin n) R))
        (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))) (RingHom.ker f.toRingHom)
obtain₁₁ obtain₁₂ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    let RXn := MvPolynomial (Fin n) R;
    let RXm := MvPolynomial (Fin m) R;
    ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
      (hg :
        ∀ (i : Fin n),
          Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
            ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
      (h : (i : Fin m) → MvPolynomial (Fin n) R)
      (hh :
        ∀ (i : Fin m),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
      let aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h;
      let g' : Fin n → RXn := fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn);
      ∀
        (hh' :
          ∀ (x : RXm),
            Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
              ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)),
        Eq (α := Ideal (MvPolynomial (Fin n) R))
          (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))) (RingHom.ker f.toRingHom)
obtain₁₃ :
  ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
    (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
    (s : Finset (MvPolynomial (Fin m) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
        (RingHom.ker f'.toRingHom)),
    let RXn := MvPolynomial (Fin n) R;
    let RXm := MvPolynomial (Fin m) R;
    ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
      (hg :
        ∀ (i : Fin n),
          Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
            ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
      (h : (i : Fin m) → MvPolynomial (Fin n) R)
      (hh :
        ∀ (i : Fin m),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
      let aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h;
      let g' : Fin n → RXn := fun (i : Fin n) ↦
        HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn);
      ∀
        (hh' :
          ∀ (x : RXm),
            Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
              ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)),
        let s' := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm);
        ∀ (leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)),
          Eq (α := Ideal (MvPolynomial (Fin n) R))
            (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))) (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have obtain₁₄ : ∀ (m : ℕ) (f' : MvPolynomial (Fin m) R →ₐ[R] A)
  (hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A))
  (s : Finset (MvPolynomial (Fin m) R))
  (hs :
    Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R)))
      (RingHom.ker f'.toRingHom)),
  let RXn := MvPolynomial (Fin n) R;
  let RXm := MvPolynomial (Fin m) R;
  ∀ (g : (i : Fin n) → MvPolynomial (Fin m) R)
    (hg :
      ∀ (i : Fin n),
        Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
          ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A))
    (h : (i : Fin m) → MvPolynomial (Fin n) R)
    (hh :
      ∀ (i : Fin m),
        Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
          ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)),
    let aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h;
    let g' : Fin n → RXn := fun (i : Fin n) ↦
      HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn);
    ∀
      (hh' :
        ∀ (x : RXm),
          Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
            ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)),
      let s' := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm);
      ∀ (leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)),
        LE.le (α := Ideal RXn) (RingHom.ker f.toRingHom) (Ideal.span s')
Tactic: classical
    obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)
    let RXn := MvPolynomial (Fin n) R
    let RXm := MvPolynomial (Fin m) R
    have := fun i : Fin n => hf' (f <| X i)
    choose g hg using this
    have := fun i : Fin m => hf (f' <| X i)
    choose h hh using this
    let aeval_h : RXm →ₐ[R] RXn := aeval h
    let g' : Fin n → RXn := fun i => X i - aeval_h (g i)
    refine ⟨Finset.univ.image g' ∪ s.image aeval_h, ?_⟩
    simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]
    have hh' : ∀ x, f (aeval_h x) = f' x := by
      intro x
      rw [← f.coe_toRingHom, map_aeval]
      simp_rw [AlgHom.coe_toRingHom, hh]
      rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
        -- Porting note: added line below
        ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
        ← aeval_unique]
    let s' := Set.range g' ∪ aeval_h '' s
    have leI : Ideal.span s' ≤ RingHom.ker f.toRingHom := by
      rw [Ideal.span_le]
      rintro _ (⟨i, rfl⟩ | ⟨x, hx, rfl⟩)
      · change f (g' i) = 0
        rw [map_sub, ← hg, hh', sub_self]
      · change f (aeval_h x) = 0
        rw [hh']
        change x ∈ RingHom.ker f'.toRingHom
        rw [← hs]
        exact Ideal.subset_span hx
    apply leI.antisymm
    intro x hx
    have : x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid := by
      have : x ∈ adjoin R (Set.range X : Set RXn) := by
        rw [adjoin_range_X]
        trivial
      refine adjoin_induction ?_ ?_ ?_ ?_ this
      · rintro _ ⟨i, rfl⟩
        rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · apply Submodule.subset_span
          apply Set.mem_union_left
          exact Set.mem_range_self _
      · intro r
        apply AddSubmonoid.mem_sup_left
        exact ⟨C r, aeval_C _ _⟩
      · intro _ _ _ _ h₁ h₂
        exact add_mem h₁ h₂
      · intro p₁ p₂ _ _ h₁ h₂
        obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
        obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
        rw [mul_add, add_mul, add_assoc, ← map_mul]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)
    obtain ⟨_, ⟨x, rfl⟩, y, hy, rfl⟩ := AddSubmonoid.mem_sup.mp this
    refine add_mem ?_ hy
    simp only [RXn, RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_add,
      show f y = 0 from leI hy, add_zero, hh'] at hx
    suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h by
      apply this
      rwa [hs]
    rw [Ideal.span_le]
    intro x hx
    apply Submodule.subset_span
    apply Set.mem_union_right
    exact Set.mem_image_of_mem _ hx