PullbackPasting.lean

import Mathlib
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

open CategoryTheory
open Limits

section PB2

variable [Category 𝓒] (A B C D E F : 𝓒)
variable (AB : A ⟶ B) (BC : B ⟶ C)
variable (AD : A ⟶ D) (BE : B ⟶ E) (CF : C ⟶ F)
variable (DE : D ⟶ E) (EF : E ⟶ F)


example (H1 : AD ≫ DE = AB ≫ BE) (H2 : BE ≫ EF = BC ≫ CF)
  (C₁ : IsLimit (PullbackCone.mk _ _ H1)) (C₂ : IsLimit (PullbackCone.mk _ _ H2)) :
  HasPullback (DE ≫ EF) CF
:= by
  refine { exists_limit := ⟨?_⟩ }
  have E₃ : AD ≫ (DE ≫ EF) = (AB ≫ BC) ≫ CF := by rw [<- Category.assoc, H1, Category.assoc, H2, Category.assoc]
  refine {
    cone := PullbackCone.mk _ _ E₃
    isLimit := {
      lift s := by
        simp
        have E₁ := s.π.naturality WalkingCospan.Hom.inr; simp at E₁
        rw [<- Category.assoc] at E₁
        let C₃ := (PullbackCone.mk _ _ E₁)
        have El : _ ≫ BE = _ ≫ DE := C₂.fac C₃ (WalkingCospan.left)
        let C₄ := (PullbackCone.mk _ _ El.symm)
        exact C₁.lift C₄
      fac s j := by
        simp
        have E₁ := s.π.naturality WalkingCospan.Hom.inr; simp at E₁
        rw [<- Category.assoc] at E₁
        set C₃ := (PullbackCone.mk _ _ E₁)
        have El : _ ≫ BE = _ ≫ DE := C₂.fac C₃ (WalkingCospan.left)
        let C₄ := (PullbackCone.mk _ _ El.symm)
        conv => arg 1; arg 1; change C₁.lift C₄
        have E0 := C₁.fac C₄ j
        simp at E0
        rcases j with _ | j<;> simp <;> simp at E0
        · slice_lhs 1 3 => rw [E0]; simp [C₄]
          simp
        · rcases j<;> simp<;> simp at E0
          · rw [E0]; rfl
          · slice_lhs 1 2 => rw [E0]
            simp [C₄]
            have := C₂.fac C₃ (WalkingCospan.right); simp at this
            rw [this]; rfl
      uniq s m Hm := by
        simp; simp at m Hm
        have E₁ := s.π.naturality WalkingCospan.Hom.inr; simp at E₁
        rw [<- Category.assoc] at E₁
        set C₃ := (PullbackCone.mk _ _ E₁)
        have El : _ ≫ BE = _ ≫ DE := C₂.fac C₃ (WalkingCospan.left)
        let C₄ := (PullbackCone.mk _ _ El.symm)
        conv => arg 2; change C₁.lift C₄
        have E0 : m ≫ AB = C₂.lift C₃ := by
          apply C₂.uniq C₃
          intro j
          have Hj := Hm j
          rcases j with _ | j<;> simp<;> simp at Hj
          · slice_lhs 2 3 => rw [<- H1]
            simp; rw [Hj]; simp [C₃]
          · rcases j<;> simp<;> simp at Hj
            · rw [<- H1, <- Category.assoc, Hj]; simp [C₃]
            · rw [Hj]; rfl
        apply C₁.uniq C₄
        · intro j
          have H0 := Hm none
          have Hl := Hm (WalkingCospan.left)
          have Hr := Hm (WalkingCospan.right)
          simp at H0 Hl Hr
          rcases j with _ | j<;> simp
          · simp [C₄]
            rw [<- Hl]; simp
          · rcases j<;> simp
            · rw [Hl]; rfl
            · rw [E0]; rfl
    }
  }

example (H1 : AD ≫ (DE ≫ EF) = (AB ≫ BC) ≫ CF) (H2 : BE ≫ EF = BC ≫ CF)
  (C₁ : IsLimit (PullbackCone.mk _ _ H1)) (C₂ : IsLimit (PullbackCone.mk _ _ H2)) :
  HasPullback DE BE
:= by
  refine { exists_limit := ⟨?_⟩ }
  have H0 : (AD ≫ DE) ≫ EF = (AB ≫ BC) ≫ CF := by simp; rw [H1]; simp
  let C₀ := PullbackCone.mk _ _ H0
  have En₀ := C₂.fac C₀ (WalkingCospan.one); simp at En₀
  have El₀ := C₂.fac C₀ (WalkingCospan.left); simp at El₀
  have Er₀ := C₂.fac C₀ (WalkingCospan.right); simp at Er₀
  set g := C₂.lift C₀; simp [C₀] at g
  simp [C₀] at En₀ El₀ Er₀
  use PullbackCone.mk _ _ El₀.symm
  refine {
    lift s := by
      simp
      change PullbackCone DE BE at s
      have Es := s.condition
      have E : s.fst ≫ DE ≫ EF = (s.snd ≫ BC) ≫ CF := by
        rw [<- Category.assoc, Es, Category.assoc, H2, Category.assoc]
      let C₃ := PullbackCone.mk _ _ E
      exact C₁.lift C₃
    fac s j := by
      simp
      change PullbackCone DE BE at s
      have Es := s.condition
      have E : s.fst ≫ DE ≫ EF = (s.snd ≫ BC) ≫ CF := by
        rw [<- Category.assoc, Es, Category.assoc, H2, Category.assoc]
      let C₃ := PullbackCone.mk _ _ E
      have Hf := C₁.fac C₃
      have Hn := Hf WalkingCospan.one
      have Hl := Hf WalkingCospan.left
      have Hr := Hf WalkingCospan.right
      simp at Hl Hr Hn
      set f := C₁.lift C₃; simp [C₃] at f
      simp [C₃] at Hl Hr Hn
      rcases j with _ | j<;> simp
      · rw [<- Hl, Category.assoc]
      · cases j <;> simp
        · rw [Hl]
        · apply C₂.hom_ext
          intro j
          rcases j with _ | j<;> simp
          · rw [En₀, Hn, E, Category.assoc, H2]
          · cases j<;> simp
            · rw [El₀, <-Category.assoc, Hl, Es]
            · rw [Er₀, Hr]
    uniq s m Hm := by
      simp; simp at m Hm
      have Hmn := Hm (WalkingCospan.one); simp at Hmn
      have Hml := Hm (WalkingCospan.left); simp at Hml
      have Hmr := Hm (WalkingCospan.right); simp at Hmr

      change PullbackCone DE BE at s
      have Es := s.condition
      have E₀ : s.fst ≫ DE ≫ EF = (s.snd ≫ BC) ≫ CF := by
        rw [<- Category.assoc, Es, Category.assoc, H2, Category.assoc]
      let C₃ := PullbackCone.mk _ _ E₀
      have Hf := C₁.fac C₃
      have Hn := Hf WalkingCospan.one
      have Hl := Hf WalkingCospan.left
      have Hr := Hf WalkingCospan.right
      simp at Hl Hr Hn
      set f := C₁.lift C₃; simp [C₃] at f
      simp [C₃] at Hl Hr Hn
      simp [f]
      apply C₁.uniq C₃
      intro j
      rcases j with _ | j<;> simp
      · simp [C₃, <- Category.assoc, <- Hmn]
      · cases j<;> simp [C₃]
        · rw [Hml]
        · rw [<- Hmr, Category.assoc, Er₀]
  }

end PB2