-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
h_1 :
  Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁))
    y
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx :
  (((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
          LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
        (a : LocalizedModule S M₀) → LocalizedModule S M₁)
      (mk m s) =
    y
rw :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        ((((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
              LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
            (a : LocalizedModule S M₀) → LocalizedModule S M₁)
          (mk m s)) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₁ :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₂ :
  Eq (α := LocalizedModule S M₂) (mk ((h : (a : M₁) → M₂) ((g : (a : M₀) → M₁) m : M₁)) s : LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
rw₃ : Eq (α := LocalizedModule S M₂) (mk 0 s) 0
rw₄ rw₅ : Eq (α := LocalizedModule S M₂) 0 0
⊢ Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        y :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)

Tactic:
rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]

Premises used: Iff.mpr, Exists.intro, LocalizedModule.zero_mk, DFunLike.coe, IsLocalizedModule.map_LocalizedModules, rfl