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

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

Tactic:
apply Submodule.fg_of_fg_map_of_fg_inf_ker f.range.mkQ

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

case mk.intro.intro.intro.hs2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : ({ x // x ∈ s } →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
this : Submodule.map (LinearMap.range f).mkQ (LinearMap.ker l) = ⊤
⊢ (LinearMap.ker l ⊓ LinearMap.ker (LinearMap.range f).mkQ).FG

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : N → M
hf : ∀ (b : N), l (f b) = b
⊢ ∃ f, l ∘ₗ f = linearCombination R Subtype.val

Tactic:
exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ LinearMap.range (linearCombination R Subtype.val) = ⊤

Tactic:
rw [range_linearCombination, Subtype.range_val, ← hs]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ Submodule.span R (Membership.mem s.val) = Submodule.span R ↑s

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

Tactic:
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⟩

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

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
h : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
⊢ (LinearMap.ker l).FG

Tactic:
obtain ⟨s, hs, hs'⟩ := h

Result:
case mk.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ (LinearMap.ker l).FG

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

Tactic:
rw [← top_le_iff]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : ({ x // x ∈ s } →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
⊢ ⊤ ≤ Submodule.map (LinearMap.range f).mkQ (LinearMap.ker l)

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

Tactic:
rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy

Result:
case intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
f : ({ x // x ∈ s } →₀ R) →ₗ[R] M
hf : l ∘ₗ f = linearCombination R Subtype.val
x : M
y : { x // x ∈ s } →₀ R
hy : l (x - f y) = 0
⊢ (LinearMap.range f).mkQ x ∈ Submodule.map (LinearMap.range f).mkQ (LinearMap.ker l)