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

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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
⊢ FinitePresentation R N

Tactic:
refine ⟨(Set.finite_range (l ∘ b)).toFinset,
  by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩

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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Proof state:
case h.e'_6.h.mp
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : { x // x ∈ ⋯.toFinset } →₀ R
⊢ (linearCombination R Subtype.val) x = 0 → ∃ y, l y = 0 ∧ f y = x

Tactic:
intro hx

Result:
case h.e'_6.h.mp
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : { x // x ∈ ⋯.toFinset } →₀ R
hx : (linearCombination R Subtype.val) x = 0
⊢ ∃ y, l y = 0 ∧ f y = x

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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
⊢ FinitePresentation R N

Tactic:
have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)

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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
⊢ FinitePresentation R N

Proof state:
case h.e'_6.h.mpr.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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
y : M
hy : l y = 0
⊢ (linearCombination R Subtype.val) (f y) = 0

Tactic:
simp [f, hπ, ← Finsupp.apply_linearCombination, hy]

Result:
no goals

Proof state:
case h.e'_6.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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : { x // x ∈ ⋯.toFinset } →₀ R
⊢ (linearCombination R Subtype.val) x = 0 ↔ ∃ y, l y = 0 ∧ f y = x

Tactic:
constructor

Result:
case h.e'_6.h.mp
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : { x // x ∈ ⋯.toFinset } →₀ R
⊢ (linearCombination R Subtype.val) x = 0 → ∃ y, l y = 0 ∧ f y = x

case h.e'_6.h.mpr
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : (LinearMap.ker l).FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → { x // x ∈ ⋯.toFinset } := fun i => ⟨l (b i), ⋯⟩
σ : { x // x ∈ ⋯.toFinset } → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : { x // x ∈ ⋯.toFinset }), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
x : { x // x ∈ ⋯.toFinset } →₀ R
⊢ (∃ y, l y = 0 ∧ f y = x) → (linearCombination R Subtype.val) x = 0