awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : Module.FinitePresentation R N
H :
  ∀ (I : Ideal R) (x : I.IsMaximal),
    ∃ (g :
      LinearMap (R := Localization.AtPrime I) (RingHom.id (Localization.AtPrime I)) (LocalizedModule I.primeCompl N)
        (LocalizedModule I.primeCompl M)),
      (LocalizedModule.map I.primeCompl :
              (a : M →ₗ[R] N) →
                LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            f ∘ₗ
          g =
        id
I : Ideal R
hI : I.IsMaximal
this :
  Membership.mem (γ :=
    Submodule (Localization (M := R) I.primeCompl)
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (range (R := Localization (M := R) I.primeCompl) (M :=
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
      (τ₁₂ := RingHom.id (Localization (M := R) I.primeCompl))
      ((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N) :
          (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        ((LocalizedModule.map I.primeCompl :
            (a : M →ₗ[R] N) →
              LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          f)))
    id
c : ↥I.primeCompl
g : N →ₗ[R] M
⊢ ∀ (x : ↥I.primeCompl),
    IsUnit (M := Module.End R (LocalizedModule I.primeCompl N))
      ((algebraMap R (Module.End R (LocalizedModule I.primeCompl N)) :
            (a : R) → Module.End R (LocalizedModule I.primeCompl N))
          (↑x : R) :
        Module.End R (LocalizedModule I.primeCompl N))

Tactic:
exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)

Premises used: LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : Module.FinitePresentation R N
H :
  ∀ (I : Ideal R) (x : I.IsMaximal),
    ∃ (g :
      LinearMap (R := Localization.AtPrime I) (RingHom.id (Localization.AtPrime I)) (LocalizedModule I.primeCompl N)
        (LocalizedModule I.primeCompl M)),
      (LocalizedModule.map I.primeCompl :
              (a : M →ₗ[R] N) →
                LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            f ∘ₗ
          g =
        id
I : Ideal R
hI : I.IsMaximal
this :
  Membership.mem (γ :=
    Submodule (Localization (M := R) I.primeCompl)
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (range (R := Localization (M := R) I.primeCompl) (M :=
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
      (τ₁₂ := RingHom.id (Localization (M := R) I.primeCompl))
      ((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N) :
          (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        ((LocalizedModule.map I.primeCompl :
            (a : M →ₗ[R] N) →
              LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          f)))
    id
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ∀ (x : ↥I.primeCompl),
    IsUnit (M := Module.End R (LocalizedModule I.primeCompl N))
      ((algebraMap R (Module.End R (LocalizedModule I.primeCompl N)) :
            (a : R) → Module.End R (LocalizedModule I.primeCompl N))
          (↑x : R) :
        Module.End R (LocalizedModule I.primeCompl N))

Tactic:
IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)

Premises used: LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : Module.FinitePresentation R N
H :
  ∀ (I : Ideal R) (x : I.IsMaximal),
    ∃ (g :
      LinearMap (R := Localization.AtPrime I) (RingHom.id (Localization.AtPrime I)) (LocalizedModule I.primeCompl N)
        (LocalizedModule I.primeCompl M)),
      (LocalizedModule.map I.primeCompl :
              (a : M →ₗ[R] N) →
                LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            f ∘ₗ
          g =
        id
I : Ideal R
hI : I.IsMaximal
this :
  Membership.mem (γ :=
    Submodule (Localization (M := R) I.primeCompl)
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (range (R := Localization (M := R) I.primeCompl) (M :=
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
      (τ₁₂ := RingHom.id (Localization (M := R) I.primeCompl))
      ((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N) :
          (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        ((LocalizedModule.map I.primeCompl :
            (a : M →ₗ[R] N) →
              LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          f)))
    id
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ∀ (x : ↥I.primeCompl),
    IsUnit (M := Module.End R (LocalizedModule I.primeCompl N))
      ((algebraMap R (Module.End R (LocalizedModule I.primeCompl N)) :
            (a : R) → Module.End R (LocalizedModule I.primeCompl N))
          (↑x : R) :
        Module.End R (LocalizedModule I.primeCompl N))

Tactic:
exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)

Premises used: LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
⊢ Module.Finite R M

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
⊢ Module.Finite R M

Tactic:
have : Module.Finite R M := by infer_instance
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
this : Module.Finite R M
obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤), Projective R M
⊢ Projective R M

Tactic:
obtain ⟨s, hs⟩ := this
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
rw : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
⊢ Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)

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

Premises used: Subtype.range_val, LinearMap.range_eq_top, Finsupp.range_linearCombination
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤

Tactic:
hs
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤

Tactic:
convert! hs
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)

Tactic:
have hf : Function.Surjective f := by
    rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, Subtype.range_val]
    convert! hs
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
hf : Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)
⊢ ∀ (I : Ideal R) (hI : I.IsMaximal),
    ∃ (h :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl M) (LocalizedModule I.primeCompl N)),
      (LocalizedModule.map I.primeCompl :
              (a : N →ₗ[R] M) →
                LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl M)
            f ∘ₗ
          h =
        LinearMap.id

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)
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
hf : Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)
this :
  ∀ (I : Ideal R) (hI : I.IsMaximal),
    ∃ (h :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl M) (LocalizedModule I.primeCompl N)),
      (LocalizedModule.map I.primeCompl :
              (a : N →ₗ[R] M) →
                LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl M)
            f ∘ₗ
          h =
        LinearMap.id
obtain : ∀ (g : M →ₗ[R] N) (hg : f ∘ₗ g = LinearMap.id), Projective R M
⊢ Projective R M

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

Premises used: LinearMap.split_surjective_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
hf : Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)
this :
  ∀ (I : Ideal R) (hI : I.IsMaximal),
    ∃ (h :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl M) (LocalizedModule I.primeCompl N)),
      (LocalizedModule.map I.primeCompl :
              (a : N →ₗ[R] M) →
                LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl M)
            f ∘ₗ
          h =
        LinearMap.id
g : M →ₗ[R] N
hg : f ∘ₗ g = LinearMap.id
⊢ Projective R M

Tactic:
Module.Projective.of_split _ _ hg

Premises used: Module.Projective.of_split
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst_3 : FinitePresentation R M
s : Finset M
hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤
N : Type (max u_1 uM) := Finsupp.{uM, u_1} (↥s) R
f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
hf : Function.Surjective (α := N) (β := M) (⇑f : (a : N) → M)
this :
  ∀ (I : Ideal R) (hI : I.IsMaximal),
    ∃ (h :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl M) (LocalizedModule I.primeCompl N)),
      (LocalizedModule.map I.primeCompl :
              (a : N →ₗ[R] M) →
                LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl M)
            f ∘ₗ
          h =
        LinearMap.id
g : M →ₗ[R] N
hg : f ∘ₗ g = LinearMap.id
⊢ Projective R M

Tactic:
exact Module.Projective.of_split _ _ hg

Premises used: Module.Projective.of_split
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
H₁ : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
⊢ Projective R M

Tactic:
apply Module.projective_of_localization_maximal

Premises used: Module.projective_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : RingEquiv.{u_4, u_1} (Rₚ P) (Localization.AtPrime P) :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P))
⊢ Projective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
Module.Projective.of_equiv (M := Mₚ P) (R := Rₚ P)
    (σ := e)
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }

Premises used: LinearEquiv.right_inv, LinearEquiv.mk, IsLocalizedModule.linearEquiv, LinearEquiv.left_inv, LinearMap.toAddHom, LinearEquiv.invFun, Module.Projective.of_equiv, LinearEquiv.toLinearMap, LinearMap.mk, LocalizedModule.mkLinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : RingEquiv.{u_4, u_1} (Rₚ P) (Localization.AtPrime P) :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P))
H₁ :
  ∀ (m : Rₚ P) (x : Mₚ P),
    AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        (m • x) =
      HSMul.hSMul (α := Localization.AtPrime P)
        ((((↑e : RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
                RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
              (a : Rₚ P) → Localization.AtPrime P)
            m :
          Localization.AtPrime P)
        (AddHom.toFun
          (LinearMap.toAddHom
            (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
              Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
          x)
⊢ Projective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
refine Module.Projective.of_equiv (M := Mₚ P) (R := Rₚ P)
    (σ := e)
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }

Premises used: LinearEquiv.right_inv, LinearEquiv.mk, IsLocalizedModule.linearEquiv, LinearEquiv.left_inv, LinearMap.toAddHom, LinearEquiv.invFun, Module.Projective.of_equiv, LinearEquiv.toLinearMap, LinearMap.mk, LocalizedModule.mkLinearMap, Ideal.primeCompl