-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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
inst_5 : Free R M
inst_6 : Module.Finite 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
let let₁ let₂ let₃ : FinitePresentation R N
let₄ :
  let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
  let π :
    Free.ChooseBasisIndex R M →
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯) :=
    fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯;
  ∀ (this : Function.Surjective π), FinitePresentation R N
⊢ FinitePresentation R N
have let₅ : let b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M;
let π :
  Free.ChooseBasisIndex R M →
    ↥(Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
  Subtype.mk (p := fun (x : N) ↦
    Membership.mem (γ := Finset N)
      (Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)
      x)
    ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) sorry;
∀
  (σ :
    (b :
        ↥(Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            sorry)) →
      Free.ChooseBasisIndex R M)
  (hσ :
    ∀
      (b_1 :
        ↥(Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            sorry)),
      π (σ b_1) = b_1),
  FinitePresentation R N
Tactic: classical
  let b := Module.Free.chooseBasis R M
  let π : Free.ChooseBasisIndex R M → (Set.finite_range (l ∘ b)).toFinset :=
    fun i ↦ ⟨l (b i), by simp⟩
  have : π.Surjective := fun ⟨x, hx⟩ ↦ by
    obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
    exact ⟨y, rfl⟩
  choose σ hσ using this
  have hπ : Subtype.val ∘ π = l ∘ b := rfl
  have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)
  have hσ₂ : l ∘ b ∘ σ = Subtype.val := by ext i; exact congr_arg Subtype.val (hσ i)
  refine ⟨(Set.finite_range (l ∘ b)).toFinset,
    by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩
  let f : M →ₗ[R] (Set.finite_range (l ∘ b)).toFinset →₀ R :=
    Finsupp.lmapDomain _ _ π ∘ₗ b.repr.toLinearMap
  convert! hl'.map f
  ext x; simp only [LinearMap.mem_ker, Submodule.mem_map]
  constructor
  · intro hx
    refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩
    · simp [Finsupp.apply_linearCombination, hσ₂, hx]
    · simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
      rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]
  · rintro ⟨y, hy, rfl⟩
    simp [f, hπ, ← Finsupp.apply_linearCombination, hy]