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

Proof state:
case H.intro.intro.a
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ ↑s •
      (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))
        (IsLocalization.mk' (Rₚ P) r s • m) =
    ↑s •
      (IsLocalization.map (Localization.AtPrime P) (RingHom.id R) ⋯) (IsLocalization.mk' (Rₚ P) r s) •
        (IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) m

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
  IsLocalization.map_id_mk']

Result:
no goals

Proof state:
case H
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑__spread✝⁻⁰).toFun (m • x) =
      ↑(IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv m • (↑__spread✝⁻⁰).toFun x

Tactic:
intros r m

Result:
case H
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
r : Rₚ P
m : Mₚ P
⊢ (↑__spread✝⁻⁰).toFun (r • m) =
    ↑(IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv r • (↑__spread✝⁻⁰).toFun m

Proof state:
case H
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
⊢ Projective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
refine Module.Projective.of_ringEquiv (M := Mₚ P)
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
  { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
      (LocalizedModule.mkLinearMap P.primeCompl M)
    map_smul' := ?_ }

Result:
case H
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑__spread✝⁻⁰).toFun (m • x) =
      ↑(IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv m • (↑__spread✝⁻⁰).toFun x