∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_7} {M₂ : Type u_5} {M₃ : Type u_4} {N₁ : Type u_8} {N₂ : Type u_9}
  {N₃ : Type u_10} [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₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (σ : M₃ → M₂) (hσ : ⇑f₂ ∘ σ = id) (ρ : N₂ → N₁)
  (hρ : ρ ∘ ⇑g₁ = id) {K₂ : Type u_2} {K₃ : Type u_3} {C₁ : Type u_6} [inst_13 : AddCommGroup K₂]
  [inst_14 : Module R K₂] [inst_15 : AddCommGroup K₃] [inst_16 : Module R K₃] [inst_17 : AddCommGroup C₁]
  [inst_18 : Module R C₁] (ι₂ : K₂ →ₗ[R] M₂),
  Function.Exact ⇑ι₂ ⇑i₂ →
    ∀ (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃) (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⋯ ⋯) (F : ⋯), ⋯