-- 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
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)
⊢ 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
have 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)))
          sorry))
      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)))
              sorry))
          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)))
                sorry)
              x))))
      x ↔
    x ∈ Submodule.map f l.ker
Tactic: ext x