-- 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
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
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : 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)
f : M →ₗ[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 :=
  lmapDomain R R π ∘ₗ (↑b.repr : M →ₗ[R] Free.ChooseBasisIndex R M →₀ R)
h :
  ∀
    (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
⊢ 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

Tactic:
ext x