-- 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
⊢ Submodule.span R (Membership.mem s.val) = Submodule.span R ↑s

Tactic:
rfl

Result:
no goals

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 ⋯
⊢ π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f

Tactic:
ext

Result:
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✝

Proof state:
case hs1
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)
⊢ ⊤.FG

Tactic:
exact Module.Finite.fg_top

Result:
no goals

Proof state:
case hs1
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)
⊢ (Submodule.map l ⊤).FG

Tactic:
rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]

Result:
case hs1
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)
⊢ ⊤.FG

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
⊢ LinearMap.range f = ⊤

Tactic:
apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)

Result:
case a
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
⊢ Submodule.map (LinearMap.ker l).subtype (LinearMap.range f) = Submodule.map (LinearMap.ker l).subtype ⊤

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
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
have hf : Function.Surjective f := by
  rw [← LinearMap.range_eq_top]
  apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
  rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
    LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
    Submodule.map_comap_eq_of_surjective H]

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 (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
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
have H : Function.Surjective π :=
  LinearMap.range_eq_top.mp
    (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)

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 ⇑π
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG