awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
x : MaximalSpectrum R
h₁ :
  Eq (α := Subalgebra R (FractionRing R)) (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯)
    (subalgebra (FractionRing R) x.asIdeal.primeCompl ⋯)
h₂ h₃ :
  Eq (α := Subalgebra R (FractionRing R))
    (subalgebra (FractionRing R) { asIdeal := x.asIdeal, isPrime := ⋯ }.asIdeal.primeCompl ⋯)
    (subalgebra (FractionRing R) x.asIdeal.primeCompl ⋯)
⊢ Eq (α := Subalgebra R (FractionRing R))
    (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
    (subalgebra.ofField (FractionRing R) x.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))

Tactic:
rw [subalgebra.ofField_eq, MaximalSpectrum.toPrimeSpectrum]

Premises used: MaximalSpectrum.toPrimeSpectrum, Localization.subalgebra.ofField_eq
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
⊢ OfLocalizationMaximal.{u_3} fun (R : Type u_3) (x : CommRing R) ↦ ∀ [IsDomain R], IsIntegrallyClosed R

Tactic:
fun _ _ h _ ↦ IsIntegrallyClosed.of_localization_maximal fun p _ hpm ↦ h p hpm

Premises used: IsIntegrallyClosed.of_localization_maximal, OfLocalizationMaximal
-- Module: Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_2 : (P : Ideal R) → [inst_5 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_3 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
inst_4 : IsDomain R
h : ∀ (P : Ideal R) [inst : P.IsMaximal], IsIntegrallyClosed.{u_3} (Rₚ P)
⊢ IsIntegrallyClosed R

Tactic:
.of_localization_maximal
  (fun P _ _ ↦ .of_equiv <| ringEquivOfRingEquiv (Rₚ P) _ (RingEquiv.refl R) P.primeCompl.map_id)

Premises used: RingEquiv.refl, IsIntegrallyClosed.of_localization_maximal, Localization.AtPrime, Submonoid.map_id, IsLocalization.ringEquivOfRingEquiv, IsIntegrallyClosed.of_equiv, Ideal.primeCompl
-- 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
Rₛ : Type u_4
Mₛ : Type u_5
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
⊢ Free Rₛ Mₛ

Tactic:
Free.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv

Premises used: IsLocalizedModule.isBaseChange, Module.Free.of_equiv, IsBaseChange.equiv
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
a :
  Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
⊢ Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)

Tactic:
apply Cardinal.lift_injective.{max uM' uR'}
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
⊢ Nontrivial R

Tactic:
have := (algebraMap R Rₛ).domain_nontrivial
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))

Tactic:
have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
a :
  ∀ (this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)),
    Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
simp only [rank_tensorProduct, rank_self,
    Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢

Premises used: Cardinal.lift_lift, rank_tensorProduct, Module.rank_self, Cardinal.lift_one, one_mul
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)

Tactic:
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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
h : Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}
⊢ Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)

Tactic:
convert! 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}

Tactic:
Cardinal.lift_umax

Premises used: Cardinal.lift_umax
-- 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
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}

Tactic:
exact Cardinal.lift_umax

Premises used: Cardinal.lift_umax
-- 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
Rₛ : Type u_4
Mₛ : Type u_5
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
⊢ finrank Rₛ Mₛ = finrank R M

Tactic:
simpa using congr(Cardinal.toNat $(Module.lift_rank_of_isLocalizedModule_of_free Rₛ S f))
-- 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
Rₛ : Type u_4
Mₛ : Type u_5
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Projective R M
⊢ Projective Rₛ Mₛ

Tactic:
Projective.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv

Premises used: IsLocalizedModule.isBaseChange, Module.Projective.of_equiv, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
N' : Type u_3
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
inst_7 : Module.Projective R M
⊢ Module.Projective (Localization (M := R) S) (LocalizedModule S M)

Tactic:
Module.projective_of_isLocalizedModule S (LocalizedModule.mkLinearMap S M)

Premises used: Module.projective_of_isLocalizedModule, LocalizedModule.mkLinearMap
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
N' : Type u_3
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
S : Submonoid R
A : Type u_4
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Module.Projective R A
⊢ Module.Projective.{u_1, u_4} (Localization (M := R) S) (Localization (M := A) (Algebra.algebraMapSubmonoid A S))

Tactic:
Module.projective_of_isLocalizedModule S (IsScalarTower.toAlgHom R A _).toLinearMap

Premises used: AlgHom.toLinearMap, Module.projective_of_isLocalizedModule, IsScalarTower.toAlgHom
-- 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
change :
  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
⊢ ∃ (g : N →ₗ[R] M), f ∘ₗ g = id

Tactic:
change LinearMap.id ∈ LinearMap.range (LinearMap.llcomp R N M N f)

Premises used: LinearMap.id, LinearMap.range, LinearMap.llcomp, DFunLike.coe
-- 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
⊢ 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

Tactic:
Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _
    fun I hI ↦ ?_

Premises used: Submodule.mem_of_localization_maximal, LocalizedModule.map, Ideal.primeCompl
-- 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
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))
⊢ 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

Tactic:
refine Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _
    fun I hI ↦ ?_

Premises used: Submodule.mem_of_localization_maximal, LocalizedModule.map, Ideal.primeCompl
-- 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
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
⊢ 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:
rw [LocalizedModule.map_id]

Premises used: LocalizedModule.map_id
-- 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
⊢ 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
-- 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:
IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)

Premises used: LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units