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

Tactic:
refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩

Result:
case h.e'_6.h.mp.refine_1
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
⊢ l (b.repr.symm (mapDomain σ x)) = 0

case h.e'_6.h.mp.refine_2
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
⊢ f (b.repr.symm (mapDomain σ x)) = 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), ⋯⟩
this : Function.Surjective π
⊢ FinitePresentation R N

Tactic:
choose σ hσ using this

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
⊢ FinitePresentation R N

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

Tactic:
exact congr_arg Subtype.val (hσ i)

Result:
no goals

Proof state:
case h.e'_6.h.mp.refine_2
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
⊢ f (b.repr.symm (mapDomain σ x)) = x

Tactic:
simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
  LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]

Result:
case h.e'_6.h.mp.refine_2
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
⊢ mapDomain π (mapDomain σ x) = x

Proof state:
case h.e'_6.h.mp.refine_1
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
⊢ l (b.repr.symm (mapDomain σ x)) = 0

Tactic:
simp [Finsupp.apply_linearCombination, hσ₂, hx]

Result:
no goals