-- Mathlib/Algebra/Module/LocalizedModule/Exact.lean
/-- Localization of modules is an exact functor, proven here for `LocalizedModule`.
See `IsLocalizedModule.map_exact` for the more general version. -/
lemma LocalizedModule.map_exact (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Exact g h) :
    Exact (map S (mkLinearMap S M₀) (mkLinearMap S M₁) g)
    (map S (mkLinearMap S M₁) (mkLinearMap S M₂) h) :=
  fun y ↦ Iff.intro
    (induction_on
      (fun m s hy ↦ by
        rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
        obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
        rw [smul_zero, mk_smul, ← LinearMap.map_smul, ex (a • m)] at ha
        rcases ha with ⟨x, hx⟩
        use mk x (⟨a, aS⟩ * s)
        rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul])
      y)
    fun ⟨x, hx⟩ ↦ by
      revert hx
      refine induction_on (fun m s hx ↦ ?_) x
      rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y →
    ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
refine induction_on (fun m s hx ↦ ?_) x

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
revert hx

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y →
    ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0