-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
obtain :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))),
    FinitePresentation R N
obtain₁ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker), FinitePresentation R N
obtain₂ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)),
    FinitePresentation R N
obtain₃ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M)),
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
obtain₄ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M))
    (σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R)
    (hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b),
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
obtain₅ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M))
    (σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R)
    (hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b)
    (this :
      (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M) '' σ '' (↑t : Set M) =
        (↑t : Set M)),
    Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (l ∘ₗ linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
obtain₆ :
  ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))))
    (t : Finset M) (ht : Submodule.span R (↑t : Set M) = l.ker)
    (H :
      Function.Surjective (α := Finsupp.{u_2, u_1} (↥s) R) (β := M)
        (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M))
    (σ : (b : M) → Finsupp.{u_2, u_1} (↥s) R)
    (hσ : ∀ (b : M), (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : ↥s →₀ R) → M) (σ b) = b)
    (this :
      (⇑(linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s →₀ R) → M) '' σ '' (↑t : Set M) =
        (↑t : Set M)),
    (Submodule.span R (↑(Finset.image σ t) : Set (↥s →₀ R)) ⊔
        LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))).FG
⊢ FinitePresentation R N

Tactic:
classical
  obtain ⟨s, hs, hs'⟩ := h
  obtain ⟨t, ht⟩ := hl'
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
    (hl.comp H)
  choose σ hσ using (show _ from H)
  have : Finsupp.linearCombination R Subtype.val '' σ '' t = t := by
    simp only [Set.image_image, hσ, Set.image_id']
  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
    ← Finset.coe_image]
  exact Submodule.FG.sup ⟨_, rfl⟩ hs'

Premises used: Finset.coe_image, LinearMap.ker_comp, Submodule.map_span, Submodule.comap_map_eq