-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
hfp :
  ∃ (ι : Type v) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
Make :
  ∀ (ι' : Type v) (w : Fintype ι') (f : MvPolynomial ι' R →ₐ[R] A)
    (hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A))
    (hf_ker : Ideal.FG (RingHom.ker f.toRingHom)),
    ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
      Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
Make₁ :
  ∀ (ι' : Type v) (w : Fintype ι') (f : MvPolynomial ι' R →ₐ[R] A)
    (hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A))
    (hf_ker : Ideal.FG (RingHom.ker f.toRingHom)),
    ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
      Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
intro :
  ∀ (ι' : Type v) (w : Fintype ι') (f : MvPolynomial ι' R →ₐ[R] A)
    (hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A))
    (hf_ker : Ideal.FG (RingHom.ker f.toRingHom)) (val : Fintype (ι ⊕ ι')),
    ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
      Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
intro₁ :
  ∀ (ι' : Type v) (w : Fintype ι') (f : MvPolynomial ι' R →ₐ[R] A)
    (hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A))
    (hf_ker : Ideal.FG (RingHom.ker f.toRingHom)) (val : Fintype (ι ⊕ ι')),
    Ideal.FG
      (RingHom.ker (F := MvPolynomial.{v, w₁} (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R))
        (↑(↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R)) :
          MvPolynomial (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R)))
intro₂ intro₃ :
  ∀ (ι' : Type v) (w : Fintype ι') (f : MvPolynomial ι' R →ₐ[R] A)
    (hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A))
    (hf_ker : Ideal.FG (RingHom.ker f.toRingHom)) (val : Fintype (ι ⊕ ι')),
    Ideal.FG
      (RingHom.ker (F := MvPolynomial ι (MvPolynomial ι' R) →+* MvPolynomial ι A)
        (AlgHom.toRingHom (MvPolynomial.mapAlgHom f)))
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
classical
  -- Make universe level `v` explicit so it matches that of `ι`
  obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
  let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
  cases nonempty_fintype (ι ⊕ ι')
  refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
  · rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
    exact Submodule.fg_bot
  · rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
    exact hf_ker.map MvPolynomial.C

Premises used: AlgEquiv.toAlgHom_toRingHom, MvPolynomial.ker_map, AlgHom.ker_coe_equiv, AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, Submodule.fg_bot