assoc — Mathlib

Lean4
/-- If all the binary fans involved a limit cones, `BinaryFan.assoc` produces another limit cone. -/
@[simps]
protected def assoc (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) :
    IsLimit (BinaryFan.assoc Q s) where
  lift t := R.lift (BinaryFan.assocInv P t)
  fac t := by rintro ⟨⟨⟩⟩ <;> simp; apply Q.hom_ext; rintro ⟨⟨⟩⟩ <;> simp
  uniq t m
    w := by
    have h := R.uniq (BinaryFan.assocInv P t) m
    rw [h]
    rintro ⟨⟨⟩⟩ <;> simp
    · apply P.hom_ext
      rintro ⟨⟨⟩⟩ <;> simp
      · exact w ⟨.left⟩
      · replace w : m ≫ Q.lift (BinaryFan.mk (s.fst ≫ sXY.snd) s.snd) = t.π.app ⟨.right⟩ := by simpa using w ⟨.right⟩
        simp [← w]
    · replace w : m ≫ Q.lift (BinaryFan.mk (s.fst ≫ sXY.snd) s.snd) = t.π.app ⟨.right⟩ := by simpa using w ⟨.right⟩
      simp [← w]
Похожие утверждения