-- Mathlib/Algebra/Module/FinitePresentation.lean
lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
    [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
    ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
⊢ f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π

Tactic:
ext j

Result:
case h.h
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
j : { x // x ∈ σ }
⊢ ((f ∘ₗ linearCombination R i) ∘ₗ lsingle j) 1 = (((s₀ • g) ∘ₗ π) ∘ₗ lsingle j) 1

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : { x // x ∈ τ } → ↥S
hs' : ∀ (x : { x // x ∈ τ }), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i : { x // x ∈ τ }, s' i
x : { x // x ∈ σ } →₀ R
hxσ : x ∈ ↑τ
⊢ x ∈ ↑(LinearMap.ker (s₁ • linearCombination R i))

Tactic:
simp only [s₁]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : { x // x ∈ τ } → ↥S
hs' : ∀ (x : { x // x ∈ τ }), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i : { x // x ∈ τ }, s' i
x : { x // x ∈ σ } →₀ R
hxσ : x ∈ ↑τ
⊢ x ∈ ↑(LinearMap.ker ((∏ i : { x // x ∈ τ }, s' i) • linearCombination R i))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : { x // x ∈ τ } → ↥S
hs' : ∀ (x : { x // x ∈ τ }), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i : { x // x ∈ τ }, s' i
x : { x // x ∈ σ } →₀ R
hxσ : x ∈ ↑τ
⊢ x ∈ ↑(LinearMap.ker ((∏ i : { x // x ∈ τ }, s' i) • linearCombination R i))

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
  ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
s' : { x // x ∈ τ } → ↥S
hs' : ∀ (x : { x // x ∈ τ }), s' x • (linearCombination R i) ↑x = 0
s₁ : ↥S := ∏ i : { x // x ∈ τ }, s' i
x : { x // x ∈ σ } →₀ R
hxσ : x ∈ ↑τ
⊢ (∏ x ∈ Finset.univ.erase ⟨x, hxσ⟩, s' x) • s' ⟨x, hxσ⟩ • (linearCombination R i) x = 0