-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (hypothesis)
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
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
have this₁ : ∀ (x : Nₚ J),
  Eq.{u_8 + 1} (α := Lₚ J)
      ((((IsLocalizedModule.map J.primeCompl (g J) (h J) : (a : N →ₗ[R] L) → Nₚ J →ₗ[R] Lₚ J) G :
              LinearMap.{u_1, u_1, u_7, u_8} (RingHom.id R) (Nₚ J) (Lₚ J)) :
            (a : Nₚ J) → Lₚ J)
          x :
        Lₚ J)
      (0 : Lₚ J) ↔
    ∃ (y : Mₚ J),
      (((IsLocalizedModule.map J.primeCompl (f J) (g J) : (a : M →ₗ[R] N) → Mₚ J →ₗ[R] Nₚ J) F :
              LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Mₚ J) (Nₚ J)) :
            (a : Mₚ J) → Nₚ J)
          y =
        x
Tactic: simp only [mem_range, mem_ker] at this ⊢
Cleared hypotheses: this