RepresentablePreserves.lean

import Mathlib
import Mathlib.CategoryTheory.Limits.Preserves.Basic


open CategoryTheory
open Limits


example [Category 𝓒] (F : 𝓒ᵒᵖ ⥤ Type v) (HF : F.IsRepresentable) :
  PreservesLimits F
:= by
  have ⟨X, ⟨HX⟩⟩ := HF.has_representation
  constructor; unfold autoParam
  intro J HJ; constructor; unfold autoParam
  intro K; constructor
  intro c Hc; constructor
  let mkCone (s : Cone (K ⋙ F)) (x : s.pt) : Cone K := {
    pt := Opposite.op X
    π := {
      app j := (HX.homEquiv.invFun (s.π.app j x)).op
      naturality {j j'} f := by
        simp
        have E := s.π.naturality f; simp at E
        rw [E]; simp; clear E
        have E := HX.homEquiv_comp ((K.map f).unop) ( (HX.homEquiv.symm (s.π.app j x)))
        simp at E
        rw [<- E]; simp
    }
  }

  refine {
    lift s x := HX.homEquiv (Hc.lift (mkCone s x)).unop
    fac s j := by
      ext x; simp
      have E := Hc.fac (mkCone s x) j
      have H := HX.homEquiv_comp  (c.π.app j).unop (Hc.lift (mkCone s x)).unop
      simp at H
      rw [<- H, <- unop_comp, E]
      simp [mkCone]
    uniq s m Hm := by
      simp at m Hm
      ext x
      let M : Opposite.op X ⟶ c.pt := (HX.homEquiv.invFun (m x)).op
      have E := Hc.uniq (mkCone s x) M; simp at E
      rw [<- E]; simp [M]; clear E
      intro j
      have H := HX.homEquiv_comp (c.π.app j).unop M.unop; simp at H
      have H' : M ≫ c.π.app j = (HX.homEquiv.symm (F.map (c.π.app j) (HX.homEquiv M.unop))).op := by
        rw [<- H]; simp
      rw [H']; simp [mkCone]; clear H H'
      refine Quiver.Hom.unop_inj_iff.mpr ?_; simp
      rw [<- Hm]; simp [M]
  }