-- 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
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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1),
    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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)),
    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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id), 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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    Submodule.FG (M :=
      Finsupp.{u_3, u_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)))
            ⋯))
        R)
      (LinearMap.ker
        (linearCombination R
          (Subtype.val (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))))
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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    Submodule.FG (M :=
      Finsupp.{u_3, u_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)))
            ⋯))
        R)
      (LinearMap.ker
        (linearCombination R
          (Subtype.val (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))))
h :
  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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    let f := lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R);
    LinearMap.ker
        (linearCombination R
          (Subtype.val (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))) =
      Submodule.map f l.ker
h₁ h₂ :
  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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    let f := lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R);
    ∀
      (x :
        Finsupp.{u_3, u_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)))
              ⋯))
          R),
      Membership.mem (γ :=
          Submodule R
            (Finsupp.{u_3, u_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)))
                  ⋯))
              R))
          (LinearMap.ker
            (linearCombination R
              (Subtype.val (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))))
          x ↔
        x ∈ Submodule.map f l.ker
h₃ :
  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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    let f := lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R);
    ∀
      (x :
        Finsupp.{u_3, u_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)))
              ⋯))
          R),
      Eq.{u_3 + 1} (α := N)
          ((linearCombination R
                  (Subtype.val (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)) :
                (a : ↥⋯.toFinset →₀ R) → N)
              x :
            N)
          (0 : N) ↔
        ∃ (y : M), Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) y : N) (0 : N) ∧ (f : (a : M) → ↥⋯.toFinset →₀ R) y = x
h₄ :
  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)) ⋯;
  ∀
    (σ :
      (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)))
              ⋯)) →
        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)))
              ⋯)),
        π (σ b_1) = b_1)
    (hπ :
      Subtype.val (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) ∘
          π =
        Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
    (hσ₁ : π ∘ σ = id)
    (hσ₂ :
      Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
        Subtype.val (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)),
    let f := lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R);
    ∀
      (x :
        Finsupp.{u_3, u_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)))
              ⋯))
          R),
      Eq.{u_3 + 1} (α := N)
          ((linearCombination R
                  (Subtype.val (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)) :
                (a : ↥⋯.toFinset →₀ R) → N)
              x :
            N)
          (0 : N) →
        ∃ (y : M), Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) y : N) (0 : N) ∧ (f : (a : M) → ↥⋯.toFinset →₀ R) y = x
⊢ FinitePresentation R N
have h₅ : 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)
  (hπ :
    Subtype.val (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) ∘
        π =
      Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M))
  (hσ₁ : π ∘ σ = id)
  (hσ₂ :
    Function.comp (β := M) (⇑l : (a : M) → N) ((⇑b : (a : Free.ChooseBasisIndex R M) → M) ∘ σ) =
      Subtype.val (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)),
  let f := lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R);
  ∀
    (x :
      Finsupp.{u_3, u_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))
        R),
    (∃ (y : M), Eq.{u_3 + 1} (α := N) ((l : (a : M) → N) y : N) (0 : N) ∧ (f : (a : M) → ↥sorry.toFinset →₀ R) y = x) →
      Eq.{u_3 + 1} (α := N)
        ((linearCombination R
                (Subtype.val (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)) :
              (a : ↥sorry.toFinset →₀ R) → N)
            x :
          N)
        (0 : 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]