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

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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
H : Function.Surjective ⇑(linearCombination R Subtype.val)
⊢ (LinearMap.ker (l ∘ₗ linearCombination R Subtype.val)).FG

Tactic:
choose σ hσ using (show _ from H)

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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → { x // x ∈ s } →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
⊢ (LinearMap.ker (l ∘ₗ 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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
⊢ 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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
⊢ Submodule.span R (Membership.mem s.val) = Submodule.span R ↑s

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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ FinitePresentation R N

Tactic:
obtain ⟨t, ht⟩ := hl'

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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
⊢ FinitePresentation R N

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
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset M
hs : Submodule.span R ↑s = ⊤
hs' : (LinearMap.ker (linearCombination R Subtype.val)).FG
t : Finset M
ht : Submodule.span R ↑t = LinearMap.ker l
H : Function.Surjective ⇑(linearCombination R Subtype.val)
σ : M → { x // x ∈ s } →₀ R
hσ : ∀ (b : M), (linearCombination R Subtype.val) (σ b) = b
this : ⇑(linearCombination R Subtype.val) '' (σ '' ↑t) = ↑t
⊢ (Submodule.span R ↑(Finset.image σ t) ⊔ LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
exact Submodule.FG.sup ⟨_, rfl⟩ hs'

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
h : FinitePresentation R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
⊢ FinitePresentation R N

Tactic:
classical
obtain ⟨s, hs, hs'⟩ := h
obtain ⟨t, ht⟩ := hl'
have H : Function.Surjective (Finsupp.linearCombination R ((↑) : s → M)) :=
  LinearMap.range_eq_top.mp
    (by rw [range_linearCombination, Subtype.range_val, ← hs]; rfl)
apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ linearCombination R Subtype.val)
  (hl.comp H)
choose σ hσ using (show _ from H)
have : Finsupp.linearCombination R Subtype.val '' (σ '' t) = t := by
  simp only [Set.image_image, hσ, Set.image_id']
rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
  ← Finset.coe_image]
exact Submodule.FG.sup ⟨_, rfl⟩ hs'

Result:
no goals