-- Module: Mathlib.RingTheory.LocalProperties.Exactness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid L
inst_6 : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_6} R (Mₚ P)
f : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst_11 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_7} R (Nₚ P)
g : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.id R) N (Nₚ P)
inst_12 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Nₚ P) P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst_13 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst_14 : (P : Ideal R) → [inst_16 : P.IsMaximal] → Module.{u_1, u_8} R (Lₚ P)
h : (P : Ideal R) → [inst_16 : P.IsMaximal] → LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) L (Lₚ P)
inst_15 : ∀ (P : Ideal R) [inst_16 : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Lₚ P) P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst_16 : J.IsMaximal],
    Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
      (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
      (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
J : Ideal R
hJ : J.IsMaximal
this :
  ∀ (x : Nₚ J),
    Membership.mem (γ := Submodule R (Nₚ J))
        (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
        x ↔
      Membership.mem (γ := Submodule R (Nₚ J))
        (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
        x
h₁ :
  ∀ (x : Nₚ J),
    Membership.mem (γ := Submodule R (Nₚ J))
        (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
        x ↔
      Membership.mem (γ := Submodule R (Nₚ J))
        (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))
        x
⊢ Eq.{u_7 + 1} (α := Submodule R (Nₚ J))
    (ker.{u_1, u_1, u_7, u_8} (R₂ := R) (M₂ := Lₚ J) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G))
    (range.{u_1, u_1, u_6, u_7} (R := R) (M := Mₚ J) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F))

Tactic:
ext x