-- Mathlib.Algebra.Module.SnakeLemma
/-- 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 and `g₁` is injective,
then this is the linear map `K₃ → C₁` given by the snake lemma.

Also see `SnakeLemma.δ` for a computable version.
 -/
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₂ →
                                                              {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₁ ⇑π₁ →
                                                                                  Function.Surjective ⇑f₂ →
                                                                                    Function.Injective ⇑g₁ → K₃ →ₗ[R] C₁