-- 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
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

Tactic:
have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → N)) :=
  LinearMap.range_eq_top.mp
    (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)

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
H : Function.Surjective ⇑(linearCombination R Subtype.val)
⊢ (LinearMap.ker l).FG

Proof state:
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

Tactic:
rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]

Result:
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) = ⊤
⊢ (Submodule.map f (LinearMap.ker (linearCombination R Subtype.val))).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
⊢ Submodule.span R (Membership.mem s.val) = Submodule.span R ↑s

Tactic:
rfl

Result:
no goals

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 : l (x - f y) = 0
⊢ (LinearMap.range f).mkQ x ∈ Submodule.map (LinearMap.range f).mkQ (LinearMap.ker l)

Tactic:
exact ⟨_, hy, by simp⟩

Result:
no goals

Proof state:
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
H : Function.Surjective ⇑(linearCombination R Subtype.val)
⊢ (LinearMap.ker l).FG

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

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
⊢ (LinearMap.ker l).FG

Proof state:
case h.h
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
a✝ : { x // x ∈ s }
⊢ ((l ∘ₗ linearCombination R fun i => f ↑i) ∘ₗ lsingle a✝) 1 = (linearCombination R Subtype.val ∘ₗ lsingle a✝) 1

Tactic:
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
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:
rintro x -

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
x : M ⧸ LinearMap.range f
⊢ x ∈ Submodule.map (LinearMap.range f).mkQ (LinearMap.ker l)

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
x : M
y : { x // x ∈ s } →₀ R
hy : l (x - f y) = 0
⊢ (LinearMap.range f).mkQ (x - f y) = (LinearMap.range f).mkQ x

Tactic:
simp

Result:
no goals