Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
eq' :
  ↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) =
    (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I))
eq :
  LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ) =
    (IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I))
MB : Baer Rₘ Mₘ
surj :
  Function.Surjective
    ⇑((IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I)))
⊢ Function.Surjective ⇑(↑R ((LocalizedModule.map m.primeCompl) (LinearMap.lcomp R M (Submodule.subtype I))))

Tactic:
LocalizedModule.restrictScalars_map_eq m.primeCompl hM gM

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
I : Ideal R
x✝¹ : FinitePresentation R ↥I := finitePresentation_of_finite R ↥I
m : Ideal R
x✝ : m.IsMaximal
Rₘ : Type u := Localization.AtPrime m
Mₘ : Type (max u v) := LocalizedModule m.primeCompl M
f : M →ₗ[R] LocalizedModule m.primeCompl M := LocalizedModule.mkLinearMap m.primeCompl M
h : R →ₗ[R] Rₘ := Algebra.linearMap R Rₘ
Iₘ : Ideal Rₘ := Submodule.localized' Rₘ m.primeCompl h I
g : ↥I →ₗ[R] ↥Iₘ := Submodule.toLocalized' Rₘ m.primeCompl h I
gM : (↥I →ₗ[R] M) →ₗ[R] ↥Iₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl g f Rₘ
hM : (R →ₗ[R] M) →ₗ[R] Rₘ →ₗ[Rₘ] LocalizedModule m.primeCompl M :=
  IsLocalizedModule.mapExtendScalars m.primeCompl h f Rₘ
eq'' : ↑R (Submodule.subtype Iₘ) = (IsLocalizedModule.map m.primeCompl g h) (Submodule.subtype I)
eq' :
  ↑R (LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ)) =
    (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I))
eq :
  LinearMap.lcomp Rₘ Mₘ (Submodule.subtype Iₘ) =
    (IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I))
MB : Baer Rₘ Mₘ
surj :
  Function.Surjective
    ⇑((IsLocalizedModule.mapExtendScalars m.primeCompl hM gM Rₘ) (LinearMap.lcomp R M (Submodule.subtype I)))
⊢ Function.Surjective
    ⇑(↑(IsLocalizedModule.iso m.primeCompl gM).symm ∘ₗ
        (IsLocalizedModule.map m.primeCompl hM gM) (LinearMap.lcomp R M (Submodule.subtype I)) ∘ₗ
          ↑(IsLocalizedModule.iso m.primeCompl hM))