-- Mathlib/Algebra/Module/Presentation/Finite.lean
lemma finitePresentation_iff_exists_presentation :
    Module.FinitePresentation A M ↔
      ∃ (pres : Presentation.{w₀, w₁} A M), Finite pres.G ∧ Finite pres.R

Proof state:
case mp.intro.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
obtain ⟨R : Type w₁, _, relation, hR⟩ :=
  Submodule.fg_iff_exists_finite_generating_family.1
    (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var) (by
      rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))

Result:
case mp.intro.intro.intro.intro.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ Submodule.span A (Set.range { var := var, linearCombination_var_relation := ⋯ }.var) = ⊤ ∧
    LinearMap.ker { var := var, linearCombination_var_relation := ⋯ }.π =
      Submodule.span A (Set.range { G := G, R := R, relation := relation }.relation)

Tactic:
exact ⟨hG, hR.symm⟩

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
r : { G := G, R := R, relation := relation }.R
⊢ (Finsupp.linearCombination A var) ({ G := G, R := R, relation := relation }.relation r) = 0

Tactic:
rw [Submodule.ext_iff] at hR

Result:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : ∀ (x : G →₀ A), x ∈ Submodule.span A (Set.range relation) ↔ x ∈ LinearMap.ker (Finsupp.linearCombination A var)
r : { G := G, R := R, relation := relation }.R
⊢ (Finsupp.linearCombination A var) ({ G := G, R := R, relation := relation }.relation r) = 0

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ { var := var, linearCombination_var_relation := ⋯ }.IsPresentation

Tactic:
rw [Relations.Solution.isPresentation_iff]

Result:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ Submodule.span A (Set.range { var := var, linearCombination_var_relation := ⋯ }.var) = ⊤ ∧
    LinearMap.ker { var := var, linearCombination_var_relation := ⋯ }.π =
      Submodule.span A (Set.range { G := G, R := R, relation := relation }.relation)

Proof state:
case mpr.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
pres : Presentation A M
left✝ : Finite pres.G
right✝ : Finite pres.R
⊢ FinitePresentation A M

Tactic:
exact pres.finitePresentation

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
exact
 ⟨{ G := G
    R := R
    relation := relation
    var := var
    linearCombination_var_relation := fun r ↦ by
      rw [Submodule.ext_iff] at hR
      exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
    toIsPresentation := by
      rw [Relations.Solution.isPresentation_iff]
      exact ⟨hG, hR.symm⟩ },
    inferInstance, inferInstance⟩

Result:
no goals

Proof state:
case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M

Tactic:
rintro ⟨pres, _, _⟩

Result:
case mpr.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
pres : Presentation A M
left✝ : Finite pres.G
right✝ : Finite pres.R
⊢ FinitePresentation A M

Proof state:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M → ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
intro

Result:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Proof state:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
obtain ⟨G : Type w₀, _, var, hG⟩ :=
  Submodule.fg_iff_exists_finite_generating_family.1
    (finite_def.1 (inferInstanceAs (Module.Finite A M)))

Result:
case mp.intro.intro.intro
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
⊢ ∃ pres, Finite pres.G ∧ Finite pres.R

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝¹ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
R : Type w₁
w✝ : Finite R
relation : R → G →₀ A
hR : ∀ (x : G →₀ A), x ∈ Submodule.span A (Set.range relation) ↔ x ∈ LinearMap.ker (Finsupp.linearCombination A var)
r : { G := G, R := R, relation := relation }.R
⊢ (Finsupp.linearCombination A var) ({ G := G, R := R, relation := relation }.relation r) = 0

Tactic:
exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M ↔ ∃ pres, Finite pres.G ∧ Finite pres.R

Tactic:
constructor

Result:
case mp
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ FinitePresentation A M → ∃ pres, Finite pres.G ∧ Finite pres.R

case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M

Proof state:
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
a✝ : FinitePresentation A M
G : Type w₀
w✝ : Finite G
var : G → M
hG : Submodule.span A (Set.range var) = ⊤
⊢ Function.Surjective ⇑(Finsupp.linearCombination A var)

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]

Result:
no goals