-- Mathlib/Algebra/Module/FinitePresentation.lean
/-- Given a split exact sequence `0 → M → N → P → 0` with `N` finitely presented,
then `M` is also finitely presented. -/
lemma Module.finitePresentation_of_split_exact
    {P : Type*} [AddCommGroup P] [Module R P]
    [Module.FinitePresentation R N]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P) (l : P →ₗ[R] N) (hl : g ∘ₗ l = .id)
    (hf : Function.Injective f) (H : Function.Exact f g) :
    Module.FinitePresentation R M

Proof state:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (Submodule.map (↑e.symm) (Submodule.map (LinearMap.inr R M P) ⊤)).FG

Tactic:
exact .map _ (.map _ (Module.Finite.fg_top))

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (LinearMap.ker (LinearMap.fst R M P ∘ₗ ↑e)).FG

Tactic:
rw [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm,
  LinearMap.exact_iff.mp Function.Exact.inr_fst, ← Submodule.map_top]

Result:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (Submodule.map (↑e.symm) (Submodule.map (LinearMap.inr R M P) ⊤)).FG

Proof state:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
this : Module.Finite R P
⊢ FinitePresentation R M

Tactic:
obtain ⟨e, rfl, rfl⟩ := ((Function.Exact.split_tfae' H).out 0 2 rfl rfl).mp
  ⟨hf, l, hl⟩

Result:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ FinitePresentation R M

Proof state:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
⊢ FinitePresentation R M

Tactic:
have := Module.Finite.of_surjective g hg

Result:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
this : Module.Finite R P
⊢ FinitePresentation R M

Proof state:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
⊢ FinitePresentation R M

Tactic:
have hg : Function.Surjective g := Function.LeftInverse.surjective (DFunLike.congr_fun hl)

Result:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
⊢ FinitePresentation R M

Proof state:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ FinitePresentation R M

Tactic:
refine Module.finitePresentation_of_surjective (LinearMap.fst _ _ _ ∘ₗ e.toLinearMap)
  (Prod.fst_surjective.comp e.surjective) ?_

Result:
case intro.intro
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
l : P →ₗ[R] N
this : Module.Finite R P
e : N ≃ₗ[R] M × P
hf : Function.Injective ⇑(↑e.symm ∘ₗ LinearMap.inl R M P)
hl : (LinearMap.snd R M P ∘ₗ ↑e) ∘ₗ l = LinearMap.id
hg : Function.Surjective ⇑(LinearMap.snd R M P ∘ₗ ↑e)
H : Function.Exact ⇑(↑e.symm ∘ₗ LinearMap.inl R M P) ⇑(LinearMap.snd R M P ∘ₗ ↑e)
⊢ (LinearMap.ker (LinearMap.fst R M P ∘ₗ ↑e)).FG