awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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
⊢ Membership.mem (γ := Submodule R (N →ₗ[R] N))
    (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
      ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f))
    id
have refine : ∀ (I : Ideal R) (hI : I.IsMaximal),
  Membership.mem (α :=
    LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
      (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
    (γ :=
    Submodule R
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
      ((fun (P : Ideal R) (x : P.IsMaximal) ↦
          (LocalizedModule.map P.primeCompl :
            (N →ₗ[R] N) →ₗ[R]
              LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
        I hI)
      (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
        ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f)))
    (((fun (P : Ideal R) (x : P.IsMaximal) ↦
              (LocalizedModule.map P.primeCompl :
                (N →ₗ[R] N) →ₗ[R]
                  LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                    (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
            I hI :
          (a : N →ₗ[R] N) → LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        id :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
Tactic: refine Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _
    fun I hI ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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
⊢ Membership.mem (α :=
    LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
      (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
    (γ :=
    Submodule R
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
      ((fun (P : Ideal R) (x : P.IsMaximal) ↦
          (LocalizedModule.map P.primeCompl :
            (N →ₗ[R] N) →ₗ[R]
              LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
        I hI)
      (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
        ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f)))
    (((fun (P : Ideal R) (x : P.IsMaximal) ↦
              (LocalizedModule.map P.primeCompl :
                (N →ₗ[R] N) →ₗ[R]
                  LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                    (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
            I hI :
          (a : N →ₗ[R] N) → LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        id :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
have rw : Membership.mem (γ :=
  Submodule R
    (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
      (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
  (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
    ((fun (P : Ideal R) (x : P.IsMaximal) ↦
        (LocalizedModule.map P.primeCompl :
          (N →ₗ[R] N) →ₗ[R]
            LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
              (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
      I hI)
    (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
      ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f)))
  id
Tactic: rw [LocalizedModule.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
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
⊢ Membership.mem (γ :=
    Submodule R
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
      ((fun (P : Ideal R) (x : P.IsMaximal) ↦
          (LocalizedModule.map P.primeCompl :
            (N →ₗ[R] N) →ₗ[R]
              LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
        I hI)
      (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
        ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f)))
    id
have 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
Tactic: have : LinearMap.id ∈ LinearMap.range (LinearMap.llcomp _
    (LocalizedModule I.primeCompl N) _ _ (LocalizedModule.map I.primeCompl f)) := H I hI
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
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
⊢ Projective R M
have this : Module.Finite R M
Tactic: have : Module.Finite R M := by infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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
⊢ Projective R M
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤), Projective R M
Tactic: obtain ⟨s, hs⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
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))
⊢ Projective R M
have hf : 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
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)
⊢ Projective R M
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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
⊢ Projective R M
have obtain : ∀ (g : M →ₗ[R] N) (hg : f ∘ₗ g = LinearMap.id), Projective R M
Tactic: obtain ⟨g, hg⟩ := LinearMap.split_surjective_of_localization_maximal _ this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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
⊢ Projective R M
have H₁ : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
Tactic: apply Module.projective_of_localization_maximal
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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)
have 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)
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' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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))
r : Rₚ P
m : Mₚ P
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (r • m) =
    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)
          r :
        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))
        m)
have H₁ : ∀ (r : R) (s : ↥P.primeCompl),
  AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (HSMul.hSMul.{u_4, u_5, u_5} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) =
    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)
        (IsLocalization.mk' (Rₚ P) r s))
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        m)
Tactic: obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X : ModuleCat.{v, u} R
proj : Projective X
⊢ Projective ((localizedModuleFunctor S).obj X)
have this : Small.{v, u} (Localization (M := R) S)
Tactic: have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X : ModuleCat.{v, u} R
proj : Projective X
this : Small.{v, u} (Localization (M := R) S)
⊢ Projective ((localizedModuleFunctor S).obj X)
have rw : ∀ (proj : Module.Projective.{u, v} R (↑X : Type v)) (this : Small.{v, u} (Localization (M := R) S)),
  Module.Projective.{u, v} (Localization (M := R) S) (↑((localizedModuleFunctor.{v, u} S).1 X) : Type v)
Tactic: rw [← IsProjective.iff_projective] at proj ⊢
Cleared hypotheses: proj, this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
n : ℕ
S : Submonoid R
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE (M.localizedModule S) n
have this : Small.{v, u} (Localization (M := R) S)
Tactic: have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 projle : HasProjectiveDimensionLE M 0
⊢ HasProjectiveDimensionLE (M.localizedModule S) 0
have projle₁ : HasProjectiveDimensionLT M 1
Tactic: simp only [HasProjectiveDimensionLE, zero_add] at projle ⊢
Cleared hypotheses: projle
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M 0
projle : HasProjectiveDimensionLT M 1
⊢ HasProjectiveDimensionLT (M.localizedModule S) 1
have zero : ∀ (projle : Module.Projective.{u, v} R (↑M : Type v)),
  Module.Projective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)
Tactic: rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at projle ⊢
Cleared hypotheses: projle
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
have succ : ∀ (P : ModuleCat.{v, u} R) [Projective P] (f : P ⟶ M) [Epi f], HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
Tactic: rcases ModuleCat.enoughProjectives.1 M with ⟨⟨P, f⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
have T_exact : T.ShortExact
Tactic: have T_exact : T.ShortExact := { exact := ShortComplex.exact_kernel f }
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
have TS_exact : TS.ShortExact
Tactic: have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)