-- 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:
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
⊢ Function.Surjective ⇑f

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

Result:
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
⊢ Submodule.span R (Membership.mem s.val) = ⊤

Proof state:
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
⊢ Projective R M

Tactic:
have : ∃ (s : Finset M), _ := this

Result:
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
this : ∃ s, Submodule.span R ↑s = ⊤
⊢ Projective R M

Proof state:
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
⊢ Projective R M

Tactic:
have : (⊤ : Submodule R M).FG := this.fg_top

Result:
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
⊢ Projective R M

Proof state:
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
⊢ Projective R M

Tactic:
have : Module.Finite R M := by infer_instance

Result:
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
⊢ Projective R M

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

Tactic:
exact Module.Projective.of_split _ _ hg

Result:
no goals

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
⊢ Projective R M

Tactic:
have hf : Function.Surjective f := by
  rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, Subtype.range_val]
  convert hs

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
⊢ 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 = ⊤
⊢ Projective R M

Tactic:
let N := s →₀ R

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
⊢ Projective R M

Proof state:
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
⊢ Submodule.span R (Membership.mem s.val) = ⊤

Tactic:
convert hs

Result:
no goals

Proof state:
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
⊢ Module.Finite R M

Tactic:
infer_instance

Result:
no goals

Proof state:
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
this : ∃ s, Submodule.span R ↑s = ⊤
⊢ Projective R M

Tactic:
obtain ⟨s, hs⟩ := this

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 = ⊤
⊢ Projective R M