-- Mathlib/RingTheory/LocalProperties/Projective.lean
theorem Module.projective_of_localization_maximal (H : ∀ (I : Ideal R) (_ : I.IsMaximal),
    Module.Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M))
    [Module.FinitePresentation R M] : Module.Projective R M

Proof state:
case intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝¹ : Module.Finite R M
this✝ : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
this : ∀ (I : Ideal R) (hI : I.IsMaximal), ∃ h, (LocalizedModule.map I.primeCompl) f ∘ₗ h = LinearMap.id
⊢ Projective R M

Tactic:
obtain ⟨g, hg⟩ := LinearMap.split_surjective_of_localization_maximal _ this

Result:
case intro.intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝¹ : Module.Finite R M
this✝ : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
this : ∀ (I : Ideal R) (hI : I.IsMaximal), ∃ h, (LocalizedModule.map I.primeCompl) f ∘ₗ h = LinearMap.id
g : M →ₗ[R] N
hg : f ∘ₗ g = LinearMap.id
⊢ Projective R M

Proof state:
case intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝ : Module.Finite R M
this : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
⊢ Projective R M

Tactic:
let f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val : s → M)

Result:
case intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝ : Module.Finite R M
this : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Projective R M

Proof state:
case intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝ : Module.Finite R M
this : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
⊢ Projective R M

Tactic:
have (I : Ideal R) (hI : I.IsMaximal) :=
  letI := H I hI
  Module.projective_lifting_property (LocalizedModule.map I.primeCompl f) LinearMap.id
  (LocalizedModule.map_surjective _ _ hf)

Result:
case intro
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
this✝¹ : Module.Finite R M
this✝ : ⊤.FG
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max uM u_1) := { x // x ∈ s } →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
this : ∀ (I : Ideal R) (hI : I.IsMaximal), ∃ h, (LocalizedModule.map I.primeCompl) f ∘ₗ h = LinearMap.id
⊢ Projective R M