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

Tactic:
simp only [LinearMap.mem_ker, Submodule.mem_map]

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
⊢ (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 // x ∈ ⋯.toFinset }
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, l (b a) = x

Tactic:
simpa using hx

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 // x ∈ ⋯.toFinset }
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, π a = ⟨x, hx⟩

Tactic:
obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx

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✝¹ : 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 // x ∈ ⋯.toFinset }
y : Free.ChooseBasisIndex R M
hx : l (b y) ∈ ⋯.toFinset
⊢ ∃ a, π a = ⟨l (b y), hx⟩

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
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Tactic:
let f : M →ₗ[R] (Set.finite_range (l ∘ b)).toFinset →₀ R :=
  Finsupp.lmapDomain _ _ π ∘ₗ b.repr.toLinearMap

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
f : M →ₗ[R] { x // x ∈ ⋯.toFinset } →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
⊢ (LinearMap.ker (linearCombination R Subtype.val)).FG

Proof state:
case h.a
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
i : { x // x ∈ ⋯.toFinset }
⊢ ↑((π ∘ σ) i) = ↑(id i)

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

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✝¹ : 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 // x ∈ ⋯.toFinset }
y : Free.ChooseBasisIndex R M
hx : l (b y) ∈ ⋯.toFinset
⊢ ∃ a, π a = ⟨l (b y), hx⟩

Tactic:
exact ⟨y, rfl⟩

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

Tactic:
let π : Free.ChooseBasisIndex R M → (Set.finite_range (l ∘ b)).toFinset :=
  fun i ↦ ⟨l (b i), by simp⟩

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), ⋯⟩
⊢ FinitePresentation R N