LeftAdjPreservesColimit.lean

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.Preserves.Basic

open CategoryTheory
open Limits

lemma Adjunction_PreservesLimit [Category 𝓐] [Category 𝓑] (F : 𝓐 ⥤ 𝓑) (G : 𝓑 ⥤ 𝓐) (σ : F ⊣ G) :
  PreservesColimits F
:= by
  refine {
  preservesColimitsOfShape := by
    intro 𝓒 _
    refine {
      preservesColimit := by
        intro K
        refine {
          preserves {C} HC := by
            constructor
            refine {
              desc C' := by
                simp
                let D : Cocone K := {
                  pt := G.obj C'.pt
                  ι := {
                    app c := σ.unit.app (K.obj c) ≫ G.map (C'.ι.app c)
                    naturality c c' f := by
                      simp
                      have E := σ.unit.naturality
                      conv at E => arg 2; arg 2; arg 2; arg 1; simp
                      rw [<- Category.assoc, E, Category.assoc]; clear E
                      conv => arg 1; arg 2; simp; rw [<- G.map_comp]
                      congr
                      have E := C'.ι.naturality f; simp at E
                      rw [E]
                  }
                }
                exact F.map (HC.desc D) ≫ σ.counit.app C'.pt
              fac C' c := by
                simp
                rw [<- Category.assoc, <- F.map_comp]
                have E := σ.counit.naturality
                conv at E => arg 2; arg 2; arg 2; arg 2; simp
                conv at E => arg 2; arg 2; arg 2; arg 1; arg 1; simp
                rw [HC.fac]
                conv => arg 1; arg 1; simp
                rw [Category.assoc, E, <- Category.assoc]; clear E
                have E := σ.left_triangle_components
                rw [E]; simp
              uniq C' m Hm := by
                simp; simp at m Hm
                set D : Cocone K := {
                  pt := G.obj C'.pt
                  ι := {
                    app c := σ.unit.app (K.obj c) ≫ G.map (C'.ι.app c)
                    naturality c c' f := by
                      simp
                      have E := σ.unit.naturality
                      conv at E => arg 2; arg 2; arg 2; arg 1; simp
                      rw [<- Category.assoc, E, Category.assoc]; clear E
                      conv => arg 1; arg 2; simp; rw [<- G.map_comp]
                      congr
                      have E := C'.ι.naturality f; simp at E
                      rw [E]
                  }
                }
                conv => arg 2; arg 1; change F.map (HC.desc D)
                let m' : C.pt ⟶ D.pt := σ.unit.app (C.pt) ≫ G.map m
                have H : (∀ (j : 𝓒), C.ι.app j ≫ m' = D.ι.app j) := by
                  intro i; simp [D, m']
                  have E := σ.unit.naturality (C.ι.app i)
                  conv at E => arg 1; arg 1; simp
                  conv at E => arg 1; arg 2; simp [Functor.const]
                  rw [<- Category.assoc, E, Category.assoc]; clear E
                  conv => arg 1; arg 2; simp; rw [<- G.map_comp]
                  rw [Hm]
                have E := HC.uniq D m' H
                rw [<- E, F.map_comp, Category.assoc]
                have E := σ.counit.naturality m
                conv at E => arg 1; arg 1; simp
                rw [E]; clear E
                have E := σ.left_triangle_components C.pt
                rw [<- Category.assoc, E]; simp
            }
        }

      }
    }