-- 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:
case h.e'_6
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
⊢ LinearMap.ker (linearCombination R Subtype.val) = Submodule.map f (LinearMap.ker l)

Tactic:
ext x

Result:
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
⊢ x ∈ LinearMap.ker (linearCombination R Subtype.val) ↔ x ∈ Submodule.map f (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✝¹ : 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
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
convert hl'.map f

Result:
case h.e'_6
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
⊢ LinearMap.ker (linearCombination R Subtype.val) = Submodule.map f (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✝¹ : 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), ⋯⟩
⊢ FinitePresentation R N

Tactic:
have : π.Surjective := fun ⟨x, hx⟩ ↦ by
  obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
  exact ⟨y, rfl⟩

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), ⋯⟩
this : Function.Surjective π
⊢ 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
i : Free.ChooseBasisIndex R M
⊢ l (b i) ∈ ⋯.toFinset

Tactic:
simp

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✝¹ : 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
⊢ ⇑l ∘ ⇑b ∘ σ = Subtype.val

Tactic:
ext i

Result:
case 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
i : { x // x ∈ ⋯.toFinset }
⊢ (⇑l ∘ ⇑b ∘ σ) i = ↑i

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
⊢ Submodule.span R ↑⋯.toFinset = ⊤

Tactic:
simpa [Set.range_comp, LinearMap.range_eq_top]

Result:
no goals