-- Mathlib/RingTheory/LocalProperties/Projective.lean
theorem LinearMap.split_surjective_of_localization_maximal
    (f : M →ₗ[R] N) [Module.FinitePresentation R N]
    (H : ∀ (I : Ideal R) (_ : I.IsMaximal),
    ∃ (g : _ →ₗ[Localization.AtPrime I] _),
      (LocalizedModule.map I.primeCompl f).comp g = LinearMap.id) :
    ∃ (g : N →ₗ[R] M), f.comp g = LinearMap.id

Proof state:
case h.e.h.a.mp
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f✝ : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f✝ ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝))
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
hf :
  f ∈
    Submodule.localized₀ I.primeCompl ((fun P x => LocalizedModule.map P.primeCompl) I hI) (range ((llcomp R N M N) f✝))
⊢ f ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝))

Tactic:
obtain ⟨a, ha, c, rfl⟩ := hf

Result:
case h.e.h.a.mp.intro.intro.intro
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
a : N →ₗ[R] N
ha : a ∈ range ((llcomp R N M N) f)
c : ↥I.primeCompl
⊢ IsLocalizedModule.mk' ((fun P x => LocalizedModule.map P.primeCompl) I hI) a c ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))

Proof state:
case h.e.h.a.mpr.intro.intro.mk
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s) ∈
    Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) (range ((llcomp R N M N) f))

Tactic:
refine ⟨f.comp g, ⟨g, rfl⟩, s, ?_⟩

Result:
case h.e.h.a.mpr.intro.intro.mk
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s =
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s)

Proof state:
case h.a.a.h.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    range
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f))
c : ↥I.primeCompl
g : N →ₗ[R] M
x✝ : N
⊢ (↑R
          (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
                (LocalizedModule I.primeCompl N))
              ((LocalizedModule.map I.primeCompl) f))
            ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
        LocalizedModule.mkLinearMap I.primeCompl N)
      x✝ =
    (↑R ((LocalizedModule.map I.primeCompl) (((llcomp R N M N) f) g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N) x✝

Tactic:
simp only [LocalizedModule.map_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, LocalizedModule.mkLinearMap_apply, LinearMap.llcomp_apply,
  LocalizedModule.map_mk]

Result:
no goals