-- Mathlib/RingTheory/LocalProperties/Exactness.lean
lemma exact_of_isLocalized_span (H : ∀ r : s, Function.Exact
    (map (.powers r.1) (f r) (g r) F) (map (.powers r.1) (g r) (h r) 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
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
      range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
r : ↑s
this :
  ∀ (x : Nₚ r),
    x ∈ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) ↔
      x ∈ range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
⊢ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
    range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)

Tactic:
ext x

Result:
case h
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
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
      range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
r : ↑s
this :
  ∀ (x : Nₚ r),
    x ∈ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) ↔
      x ∈ range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
x : Nₚ r
⊢ x ∈ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) ↔
    x ∈ range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)

Proof state:
case h
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
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
      range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
r : ↑s
x : Nₚ r
this :
  ∀ (x : Nₚ r),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
      ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
    ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x

Tactic:
exact this x

Result:
no goals

Proof state:
case h
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
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
      range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
r : ↑s
this :
  ∀ (x : Nₚ r),
    x ∈ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) ↔
      x ∈ range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
x : Nₚ r
⊢ x ∈ ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) ↔
    x ∈ range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)

Tactic:
simp only [mem_range, mem_ker] at this ⊢

Result:
case h
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
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ker ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) =
      range ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
r : ↑s
x : Nₚ r
this :
  ∀ (x : Nₚ r),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
      ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
    ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x