-- Mathlib.Algebra.Module.SnakeLemma
/-- **Snake Lemma**
Suppose we have an exact commutative diagram
```
                K₃
                |
                ι₃
                ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁

```
such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`,
then the map `π₁ ∘ ρ ∘ i₂ ∘ σ ∘ ι₃` is a linear map from `K₃` to `C₁`.

Also see `SnakeLemma.δ'` for a noncomputable version
that does not require an explicit section and retraction.
 -/
SnakeLemma.δ : {R : Type u_1} →
  [inst : CommRing R] →
    {M₁ : Type u_2} →
      {M₂ : Type u_3} →
        {M₃ : Type u_4} →
          {N₁ : Type u_5} →
            {N₂ : Type u_6} →
              {N₃ : Type u_7} →
                [inst_1 : AddCommGroup M₁] →
                  [inst_2 : Module R M₁] →
                    [inst_3 : AddCommGroup M₂] →
                      [inst_4 : Module R M₂] →
                        [inst_5 : AddCommGroup M₃] →
                          [inst_6 : Module R M₃] →
                            [inst_7 : AddCommGroup N₁] →
                              [inst_8 : Module R N₁] →
                                [inst_9 : AddCommGroup N₂] →
                                  [inst_10 : Module R N₂] →
                                    [inst_11 : AddCommGroup N₃] →
                                      [inst_12 : Module R N₃] →
                                        (i₁ : M₁ →ₗ[R] N₁) →
                                          (i₂ : M₂ →ₗ[R] N₂) →
                                            (i₃ : M₃ →ₗ[R] N₃) →
                                              (f₁ : M₁ →ₗ[R] M₂) →
                                                (f₂ : M₂ →ₗ[R] M₃) →
                                                  Function.Exact ⇑f₁ ⇑f₂ →
                                                    (g₁ : N₁ →ₗ[R] N₂) →
                                                      (g₂ : N₂ →ₗ[R] N₃) →
                                                        Function.Exact ⇑g₁ ⇑g₂ →
                                                          g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
                                                            g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
                                                              (σ : M₃ → M₂) →
                                                                ⇑f₂ ∘ σ = id →
                                                                  (ρ : N₂ → N₁) →
                                                                    ρ ∘ ⇑g₁ = id →
                                                                      {K₃ : Type u_9} →
                                                                        {C₁ : Type u_10} →
                                                                          [inst_13 : AddCommGroup K₃] →
                                                                            [inst_14 : Module R K₃] →
                                                                              [inst_15 : AddCommGroup C₁] →
                                                                                [inst_16 : Module R C₁] →
                                                                                  (ι₃ : K₃ →ₗ[R] M₃) →
                                                                                    Function.Exact ⇑ι₃ ⇑i₃ →
                                                                                      (π₁ : N₁ →ₗ[R] C₁) →
                                                                                        Function.Exact ⇑i₁ ⇑π₁ →
                                                                                          K₃ →ₗ[R] C₁