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

Tactic:
exact hs'.map f

Result:
no goals

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

Tactic:
exact Module.Finite.fg_top

Result:
no goals

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

Tactic:
obtain ⟨y, hy⟩ := H (l x)

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

Tactic:
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x

Result:
case 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
⊢ (LinearMap.range f).mkQ 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 : N → M
hf : ∀ (b : N), l (f b) = b
⊢ (l ∘ₗ linearCombination R fun i => f ↑i) = linearCombination R Subtype.val

Tactic:
ext

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

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, l ∘ₗ f = linearCombination R Subtype.val

Tactic:
choose f hf using show _ from hl

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 : N → M
hf : ∀ (b : N), l (f b) = b
⊢ ∃ f, l ∘ₗ f = linearCombination R Subtype.val

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

Tactic:
rw [this]

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) = ⊤
⊢ ⊤.FG