-- 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:
case mk.intro.intro.intro
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
this : LinearMap.ker π ≤ LinearMap.ker (s₁ • linearCombination R i)
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
refine ⟨Submodule.liftQ _ _ this ∘ₗ
  (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩

Result:
case mk.intro.intro.intro
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
this : LinearMap.ker π ≤ LinearMap.ker (s₁ • linearCombination R i)
⊢ f ∘ₗ (LinearMap.ker π).liftQ (s₁ • linearCombination R i) this ∘ₗ ↑(π.quotKerEquivOfSurjective hπ).symm =
    (s₁ * s₀) • g

Proof state:
case h.e'_2.h.e'_21.h.h.h.h.h.h.a
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
this : LinearMap.ker π ≤ LinearMap.ker (s₁ • linearCombination R i)
x✝ : { x // x ∈ σ } →₀ R
e_7✝ : CommSemiring.toSemiring = Ring.toSemiring
e_10✝ : instAddCommMonoid = AddCommGroup.toAddCommMonoid
he✝ : RingHom.id R = RingHom.id R
x : { x // x ∈ σ }
⊢ (π.quotKerEquivOfSurjective hπ) (((↑(π.quotKerEquivOfSurjective hπ).symm ∘ₗ π) ∘ₗ lsingle x) 1) =
    (π.quotKerEquivOfSurjective hπ) (((LinearMap.ker π).mkQ ∘ₗ lsingle x) 1)

Tactic:
simp [LinearMap.quotKerEquivOfSurjective]

Result:
no goals

Proof state:
case mk.intro.intro.intro
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
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
let s₁ := ∏ i : τ, s' i

Result:
case mk.intro.intro.intro
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
⊢ ∃ h s, f ∘ₗ h = s • g

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

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
  linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
  i, s₀, π]

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 ∈ σ }
⊢ (∏ j ∈ σ.erase ↑j, (s (g j)).2) • (s (g ↑j)).2 • g ↑j = (∏ j ∈ σ, (s (g j)).2) • g ↑j