-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_2
M : Type u_3
N : Type ?u.260520
N' : Type ?u.260786
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst_7 : IsLocalizedModule S f
A : Type u_1
inst_8 : CommRing A
inst_9 : Algebra R A
inst_10 : Module.FinitePresentation R M
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)),
    Module.FinitePresentation A (A ⊗[R] M)
obtain₁ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))), Module.FinitePresentation A (A ⊗[R] M)
obtain₂ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R))),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
obtain₃ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
    (this :
      Function.Exact (M := A ⊗[R] ↥f.ker) (N := A ⊗[R] (Fin n → R)) (P := A ⊗[R] M)
        (⇑(LinearMap.baseChange A f.ker.subtype) : (a : A ⊗[R] ↥f.ker) → A ⊗[R] (Fin n → R))
        (⇑(LinearMap.baseChange A f) : (a : A ⊗[R] (Fin n → R)) → A ⊗[R] M)),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
obtain₄ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
    (this :
      Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
        (LinearMap.range (LinearMap.baseChange A f.ker.subtype))),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.ker (LinearMap.baseChange A f))
obtain₅ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
    (this :
      Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
        (LinearMap.range (LinearMap.baseChange A f.ker.subtype))),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
obtain₆ :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M))
    (inst_11 : Module.FinitePresentation A (A ⊗[R] (Fin n → R)))
    (this :
      Eq (α := Submodule A (A ⊗[R] (Fin n → R))) (LinearMap.ker (LinearMap.baseChange A f))
        (LinearMap.range (LinearMap.baseChange A f.ker.subtype)))
    (this : Module.Finite R ↥f.ker),
    Submodule.FG (M := A ⊗[R] (Fin n → R)) (LinearMap.range (LinearMap.baseChange A f.ker.subtype))
⊢ Module.FinitePresentation A (A ⊗[R] M)

Tactic:
classical
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  have inst := Module.finitePresentation_of_projective A (A ⊗[R] (Fin n → R))
  apply Module.finitePresentation_of_surjective (f.baseChange A)
    (LinearMap.lTensor_surjective A hf)
  have : Function.Exact ((LinearMap.ker f).subtype.baseChange A) (f.baseChange A) :=
    lTensor_exact A f.exact_subtype_ker_map hf
  rw [LinearMap.exact_iff] at this
  rw [this]
  have : Module.Finite R (LinearMap.ker f) :=
    .of_fg (Module.FinitePresentation.fg_ker f hf)
  exact Submodule.fg_range _

Premises used: Submodule.fg_range, Module.Finite.exists_fin', LinearMap.exact_iff