awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
refine_1 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅
    ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt
refine_2 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
      ⋯.cone.π.app WalkingCospan.left
refine_3 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
      ⋯.cone.π.app WalkingCospan.right
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
refine
    IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
      (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
        (isLimitOfPreserves F s.isLimit))

Premises used: CategoryTheory.Functor.map_commSq, CategoryTheory.Limits.cospanCompIso, CategoryTheory.IsPullback.toCommSq, CategoryTheory.IsPullback.of_isLimit', DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso, CategoryTheory.Limits.WalkingCospan.ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅
    ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
      ⋯.cone.π.app WalkingCospan.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
      ⋯.cone.π.app WalkingCospan.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
      (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
        (isColimitOfPreserves F s.isColimit))

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.IsPushout.of_isColimit', CategoryTheory.Limits.spanCompIso, CategoryTheory.Functor.map_commSq, CategoryTheory.IsPushout.toCommSq, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.WalkingSpan.ext, DFunLike.coe, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesColimit (span f g) F
s : IsPushout f g h i
refine_1 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅
    ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt
refine_2 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
    ⋯.cocone.ι.app WalkingCospan.left
refine_3 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
    ⋯.cocone.ι.app WalkingCospan.right
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
refine
    IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
      (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
        (isColimitOfPreserves F s.isColimit))

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.IsPushout.of_isColimit', CategoryTheory.Limits.spanCompIso, CategoryTheory.Functor.map_commSq, CategoryTheory.IsPushout.toCommSq, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.WalkingSpan.ext, DFunLike.coe, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅
    ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
    ⋯.cocone.ι.app WalkingCospan.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
    ⋯.cocone.ι.app WalkingCospan.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPullback f g h i

Tactic:
⟨⟨e⟩, ⟨isLimitOfReflects F <| ?_⟩⟩

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
refine : IsLimit (F.mapCone (PullbackCone.mk f g ⋯))
⊢ IsPullback f g h i

Tactic:
refine ⟨⟨e⟩, ⟨isLimitOfReflects F <| ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt ≅ H.cone.pt
refine_2 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt) ≫
      H.cone.π.app WalkingCospan.left
refine_3 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt) ≫
      H.cone.π.app WalkingCospan.right
⊢ IsLimit (F.mapCone (PullbackCone.mk f g ⋯))

Tactic:
refine
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)).symm
      H.isLimit

Premises used: CategoryTheory.Limits.cospanCompIso, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso, CategoryTheory.Limits.WalkingCospan.ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt) ≫
      H.cone.π.app WalkingCospan.left

Tactic:
(Category.comp_id _).trans (Category.id_comp _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt) ≫
      H.cone.π.app WalkingCospan.right

Tactic:
(Category.comp_id _).trans (Category.id_comp _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt ≅ H.cone.pt

Tactic:
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _).symm,
    (Category.comp_id _).trans (Category.id_comp _).symm]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Category.comp_id, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsLimit (cospan h i) F
inst_3 : F.Faithful
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa only [F.map_comp] using H.w

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : PreservesLimit (cospan h i) F
inst_3 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ IsPullback f g h i

Tactic:
⟨fun h => h.of_map F e, fun h => h.map F⟩

Premises used: CategoryTheory.IsPullback.of_map, Iff.intro, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i

Tactic:
⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩

Premises used: CategoryTheory.IsPushout.mk, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
refine : IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
⊢ IsPushout f g h i

Tactic:
refine ⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt
refine_2 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt) =
    H.cocone.ι.app WalkingCospan.left
refine_3 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt) =
    H.cocone.ι.app WalkingCospan.right
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))

Tactic:
refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.spanCompIso, CategoryTheory.IsPushout.isColimit, Equiv.symm, CategoryTheory.Limits.WalkingSpan.ext, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt) =
    H.cocone.ι.app WalkingCospan.left

Tactic:
(Category.comp_id _).trans (Category.id_comp _)

Premises used: CategoryTheory.Category.comp_id, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt) =
    H.cocone.ι.app WalkingCospan.right

Tactic:
(Category.comp_id _).trans (Category.id_comp _)

Premises used: CategoryTheory.Category.comp_id, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt

Tactic:
exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _),
    (Category.comp_id _).trans (Category.id_comp _)]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Category.comp_id, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : ReflectsColimit (span f g) F
inst_3 : F.Faithful
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa only [F.map_comp] using H.w

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.Functor.map_comp, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v₁, v_1, u₁, u_1} C D
inst_2 : PreservesColimit (span f g) F
inst_3 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ IsPushout f g h i

Tactic:
⟨fun h => h.of_map F e, fun h => h.map F⟩

Premises used: Iff.intro, CategoryTheory.IsPushout.of_map, CategoryTheory.IsPushout.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ PreservesLimit (cospan f g) F ↔ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)

Tactic:
⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩

Premises used: Iff.intro, CategoryTheory.IsPullback.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
refine : ∀ (hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)), PreservesLimit (cospan f g) F
⊢ PreservesLimit (cospan f g) F ↔ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)

Tactic:
refine ⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
apply : IsLimit (F.mapCone h.cone)
⊢ PreservesLimit (cospan f g) F

Tactic:
apply preservesLimit_of_preserves_limit_cone h.isLimit

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ IsLimit (F.mapCone h.cone)

Tactic:
exact (PullbackCone.isLimitMapConeEquiv _ _).symm hF.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
⊢ PreservesColimit (span f g) F ↔ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)

Tactic:
⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩

Premises used: Iff.intro, CategoryTheory.IsPushout.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
refine : ∀ (hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)), PreservesColimit (span f g) F
⊢ PreservesColimit (span f g) F ↔ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)

Tactic:
refine ⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
apply : IsColimit (F.mapCocone h.cocone)
⊢ PreservesColimit (span f g) F

Tactic:
apply preservesColimit_of_preserves_colimit_cocone h.isColimit

Premises used: CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ IsColimit (F.mapCocone h.cocone)

Tactic:
exact (PushoutCocone.isColimitMapCoconeEquiv _ _).symm hF.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y),
      IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
suffices : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
suffices h : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F from
    ⟨fun {K} ↦ preservesLimit_of_iso_diagram _ (Limits.diagramIsoCospan K).symm⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y),
      IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ PreservesLimit (cospan f g) F

Tactic:
.mk' fun h ↦ ?_

Premises used: CategoryTheory.Limits.PreservesLimit.mk'