-- 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 : Module.Finite R M
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
obtain :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))))),
    l.ker.FG
obtain₁ :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N)),
    l.ker.FG
obtain₂ :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N))
    (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M)
    (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))), l.ker.FG
obtain₃ :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N))
    (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M) (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))
    (this : Submodule.map f.range.mkQ l.ker = ⊤), l.ker.FG
hs1 :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N))
    (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M) (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))
    (this : Submodule.map f.range.mkQ l.ker = ⊤), (Submodule.map f.range.mkQ l.ker).FG
hs2 hs2₁ :
  ∀ (s : Finset N) (hs : Eq (α := Submodule R N) (Submodule.span R (↑s : Set N)) ⊤)
    (hs' :
      Submodule.FG (M := Finsupp.{u_3, u_1} (↥s) R)
        (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))))
    (H :
      Function.Surjective (α := Finsupp.{u_3, u_1} (↥s) R) (β := N)
        (⇑(linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s))) : (a : ↥s →₀ R) → N))
    (f : Finsupp.{u_3, u_1} (↥s) R →ₗ[R] M) (hf : l ∘ₗ f = linearCombination R (Subtype.val (p := fun (x : N) ↦ x ∈ s)))
    (this : Submodule.map f.range.mkQ l.ker = ⊤), (l.ker ⊓ f.range.mkQ.ker).FG
⊢ l.ker.FG

Tactic:
classical
  obtain ⟨s, hs, hs'⟩ := h
  have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
    LinearMap.range_eq_top.mp
      (by rw [range_linearCombination, Subtype.range_val, ← hs])
  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.linearCombination R Subtype.val) := by
    choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩
  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
    rw [← top_le_iff]
    rintro x -
    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
    obtain ⟨y, hy⟩ := H (l x)
    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
    exact ⟨_, hy, by simp⟩
  apply Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.range f).mkQ
  · rw [this]
    exact Module.Finite.fg_top
  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
    exact hs'.map f

Premises used: Module.Finite.fg_top, Submodule.map_comap_eq, LinearMap.ker_comp, inf_comm, Submodule.ker_mkQ, Finsupp.linearCombination, Subtype.val