-- Mathlib/RingTheory/LocalProperties/Exactness.lean
theorem exact_of_isLocalized_maximal (H : ∀ (J : Ideal R) [J.IsMaximal],
    Function.Exact (map J.primeCompl (f J) (g J) F) (map J.primeCompl (g J) (h J) G)) :
    Function.Exact F G

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)
Lₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_7
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) =
      range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
J : Ideal R
hJ : J.IsMaximal
⊢ ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) = range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)

Tactic:
have := SetLike.ext_iff.mp <| H J

Result:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)
Lₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_7
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) =
      range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
J : Ideal R
hJ : J.IsMaximal
this :
  ∀ (x : Nₚ J),
    x ∈ ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) ↔
      x ∈ range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
⊢ ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) = range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)
Lₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_7
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) =
      range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
J : Ideal R
hJ : J.IsMaximal
⊢ localized₀ J.primeCompl (g J) (ker G) = localized₀ J.primeCompl (g J) (range F)

Tactic:
rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f J) (g J) F,
  ← LinearMap.ker_localizedMap_eq_localized₀_ker J.primeCompl (g J) (h J) G]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
Nₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (g P)
Lₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_7
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) =
      range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
J : Ideal R
hJ : J.IsMaximal
⊢ ker ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) = range ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)