-- 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
s : Set R
spn : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_7 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
Nₚ : (↑s : Type u_1) → Type u_6
inst_10 : (r : (↑s : Type u_1)) → AddCommMonoid (Nₚ r)
inst_11 : (r : (↑s : Type u_1)) → Module.{u_1, u_6} R (Nₚ r)
g : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) N (Nₚ r)
inst_12 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (g r)
Lₚ : (↑s : Type u_1) → Type u_7
inst_13 : (r : (↑s : Type u_1)) → AddCommMonoid (Lₚ r)
inst_14 : (r : (↑s : Type u_1)) → Module.{u_1, u_7} R (Lₚ r)
h : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_4, u_7} (RingHom.id R) L (Lₚ r)
inst_15 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : (↑s : Type u_1)),
    Eq.{u_6 + 1} (α := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
r : (↑s : Type u_1)
this :
  ∀ (x : Nₚ r),
    Membership.mem (γ := Submodule R (Nₚ r))
        (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
        x ↔
      Membership.mem (γ := Submodule R (Nₚ r))
        (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
          ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
        x
x : Nₚ r
⊢ Membership.mem (γ := Submodule R (Nₚ r))
      (ker.{u_1, u_1, u_6, u_7} (R₂ := R) (M₂ := Lₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G))
      x ↔
    Membership.mem (γ := Submodule R (Nₚ r))
      (range.{u_1, u_1, u_5, u_6} (R := R) (M := Mₚ r) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F))
      x
have this₁ : ∀ (x : Nₚ r),
  Eq.{u_7 + 1} (α := Lₚ r)
      ((((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (g r) (h r) : (a : N →ₗ[R] L) → Nₚ r →ₗ[R] Lₚ r) G :
              LinearMap.{u_1, u_1, u_6, u_7} (RingHom.id R) (Nₚ r) (Lₚ r)) :
            (a : Nₚ r) → Lₚ r)
          x :
        Lₚ r)
      (0 : Lₚ r) ↔
    ∃ (y : Mₚ r),
      (((IsLocalizedModule.map (Submonoid.powers (↑r : R)) (f r) (g r) : (a : M →ₗ[R] N) → Mₚ r →ₗ[R] Nₚ r) F :
              LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ r) (Nₚ r)) :
            (a : Mₚ r) → Nₚ r)
          y =
        x
Tactic: simp only [mem_range, mem_ker] at this ⊢
Cleared hypotheses: this