inv — Mathlib

Lean4
/-- The underlying inverse of `pullbackDiagonalIso` -/
abbrev inv :
    pullback i₁ i₂ ⟶
      pullback (diagonal f)
        (map (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) f f (i₁ ≫ fst _ _) (i₂ ≫ fst _ _) i
          (by simp only [Category.assoc, condition]) (by simp only [Category.assoc, condition])) :=
  pullback.lift (pullback.fst _ _ ≫ i₁ ≫ pullback.fst _ _)
    (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.snd _ _) (Category.id_comp _).symm (Category.id_comp _).symm)
    (by
      ext
      ·
        simp only [Category.assoc, diagonal_fst, Category.comp_id, limit.lift_π, PullbackCone.mk_pt,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_left]
      ·
        simp only [condition_assoc, Category.assoc, diagonal_snd, Category.comp_id, limit.lift_π, PullbackCone.mk_pt,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_right])
Похожие утверждения