-- Mathlib/Algebra/Module/FinitePresentation.lean
lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
    (l : M →ₗ[R] N) (hl : Function.Surjective l) [Module.FinitePresentation R (LinearMap.ker l)] :
    Module.FinitePresentation R M

Proof state:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
⊢ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.range_eq_top]

Result:
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
⊢ LinearMap.range f = ⊤

Proof state:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
hf : Function.Surjective ⇑f
⊢ (LinearMap.ker π).FG

Tactic:
have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) :=
  Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))

Result:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this✝ : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π)
⊢ (LinearMap.ker π).FG

Proof state:
case h
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
x✝ : ↥(LinearMap.ker (l ∘ₗ π))
⊢ (π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype) x✝ = ((LinearMap.ker l).subtype ∘ₗ f) x✝

Tactic:
rfl

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this✝ : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
hf : Function.Surjective ⇑f
this : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π)
⊢ (Submodule.map (LinearMap.ker (l ∘ₗ π)).subtype (LinearMap.ker f)).FG

Tactic:
exact (Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)

Result:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Proof state:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
hf : Function.Surjective ⇑f
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
show (LinearMap.ker π).FG

Result:
case intro
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥(LinearMap.ker l)
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(LinearMap.ker (l ∘ₗ π))
this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance
f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯
e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f
hf : Function.Surjective ⇑f
⊢ (LinearMap.ker π).FG