awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_2 :
  ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).ι.app WalkingSpan.right
⊢ inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).inr

Tactic:
dsimp only [inr]

Premises used: CategoryTheory.Limits.PushoutCocone.inr
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.right ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).ι.app WalkingSpan.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, comm]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
none : (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj Option.none ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        Option.none ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app Option.none)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
some : (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj
        (Option.some WalkingPair.left) ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (Option.some WalkingPair.left) ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (Option.some WalkingPair.left))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
some : (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj
        (Option.some WalkingPair.right) ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (Option.some WalkingPair.right) ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (Option.some WalkingPair.right))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k

Tactic:
simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst_2 : PreservesColimit (span f g) G
l : IsColimit (PushoutCocone.mk h k comm)
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, comm]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst_2 : ReflectsColimit (span f g) G
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, comm]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst_2 : PreservesColimit (span f g) G
i : HasPushout f g
⊢ Eq (α := G.obj W ⟶ G.obj (pushout f g)) (G.map f ≫ G.map (pushout.inl f g)) (G.map g ≫ G.map (pushout.inr f g))

Tactic:
simp only [← G.map_comp, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
apply : IsColimit ((Cocone.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
⊢ IsColimit (G.mapCocone c)

Tactic:
apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
apply :
  IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯)
⊢ IsColimit ((Cocone.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))

Tactic:
apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.PushoutCocone.isoMk, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
ht :
  IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯)

Tactic:
apply PushoutCocone.isColimitOfFlip

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitOfFlip
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
ht : IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ⋯))
apply :
  (span g f).map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right =
    (span g f).map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip

Tactic:
apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun

Premises used: Equiv.toFun, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
ht : IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ⋯))
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ⋯))

Tactic:
dsimp only [span_map_fst, span_map_snd]

Premises used: CategoryTheory.Limits.span_map_snd, CategoryTheory.Limits.span_map_fst
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ⋯))

Tactic:
exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)

Premises used: CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
⊢ HasPushout (G.map f) (G.map g)

Tactic:
⟨⟨⟨_, isColimitPushoutCoconeMapOfIsColimit G _ (pushoutIsPushout _ _)⟩⟩⟩

Premises used: CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushout
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
inst_4 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := pushout (G.map f) (G.map g) ⟶ G.obj (pushout f g)) (Iso.hom (iso G f g)) (pushoutComparison G f g)

Tactic:
rfl

Premises used: CategoryTheory.Limits.pushoutComparison, CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
inst_4 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj X ⟶ G.obj (pushout f g))
    (CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g)) (Iso.hom (iso G f g)))
    (G.map (pushout.inl f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
inst_4 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj Y ⟶ G.obj (pushout f g))
    (CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g)) (Iso.hom (iso G f g)))
    (G.map (pushout.inr f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
inst_4 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj X ⟶ pushout (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (G.map (pushout.inl f g)) (Iso.inv (iso G f g)))
    (pushout.inl (G.map f) (G.map g))

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.PreservesPushout.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
inst_3 : HasPushout f g
inst_4 : HasPushout (G.map f) (G.map g)
⊢ Eq (α := G.obj Y ⟶ pushout (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (G.map (pushout.inr f g)) (Iso.inv (iso G f g)))
    (pushout.inr (G.map f) (G.map g))

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.PreservesPushout.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
i : IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
apply : IsLimit (G.mapCone (PullbackCone.mk (W := pullback f g) (pullback.fst f g) (pullback.snd f g) ⋯))
⊢ PreservesLimit (cospan f g) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (pullbackIsPullback f g)

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
i : IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
apply : IsLimit (PullbackCone.mk (W := G.obj (pullback f g)) (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) ⋯)
⊢ IsLimit (G.mapCone (PullbackCone.mk (W := pullback f g) (pullback.fst f g) (pullback.snd f g) ⋯))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
i : IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
⊢ IsLimit (PullbackCone.mk (W := G.obj (pullback f g)) (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (cospan (G.map f) (G.map g))) i

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
inst_4 : PreservesLimit (cospan f g) G
⊢ IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (Iso.hom (PreservesPullback.iso G f g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
i : IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (pushoutComparison G f g)
apply : IsColimit (G.mapCocone (PushoutCocone.mk (W := pushout f g) (pushout.inl f g) (pushout.inr f g) ⋯))
⊢ PreservesColimit (span f g) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (pushoutIsPushout f g)

Premises used: CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
i : IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (pushoutComparison G f g)
apply : IsColimit (PushoutCocone.mk (W := G.obj (pushout f g)) (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (W := pushout f g) (pushout.inl f g) (pushout.inr f g) ⋯))

Tactic:
apply (isColimitMapCoconePushoutCoconeEquiv _ _).symm _

Premises used: Equiv.symm, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
i : IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (pushoutComparison G f g)
⊢ IsColimit (PushoutCocone.mk (W := G.obj (pushout f g)) (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)

Tactic:
exact IsColimit.ofPointIso _ (i := i)

Premises used: CategoryTheory.Limits.IsColimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
inst_4 : PreservesColimit (span f g) G
⊢ IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (Iso.hom (PreservesPushout.iso G f g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
inst_4 : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ (Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (obj yoneda X)).hom).obj
      (Cone.whisker walkingSpanOpEquiv.symm.functor (mapCone (obj yoneda X) (Cocone.op c))) ≅
    mapCone (obj yoneda X) c.op

Tactic:
exact Cone.ext (Iso.refl _) (by rintro (_ | _ | _) <;> cat_disch)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
h : sq.IsPullback
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimit (cospan sq.f₂₄ sq.f₃₄) F
⊢ (sq.map F).IsPullback

Tactic:
Square.IsPullback.mk _ (isLimitPullbackConeMapOfIsLimit F sq.fac h.isLimit)

Premises used: CategoryTheory.Square.IsPullback.mk, CategoryTheory.Square.IsPullback.isLimit, CategoryTheory.Square.fac, CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : ReflectsLimit (cospan sq.f₂₄ sq.f₃₄) F
h : (sq.map F).IsPullback
⊢ sq.IsPullback

Tactic:
CategoryTheory.IsPullback.of_map F sq.fac h

Premises used: CategoryTheory.IsPullback.of_map, CategoryTheory.Square.fac, CategoryTheory.Square.IsPullback
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesLimit (cospan sq.f₂₄ sq.f₃₄) F
inst_3 : ReflectsLimit (cospan sq.f₂₄ sq.f₃₄) F
⊢ (sq.map F).IsPullback ↔ sq.IsPullback

Tactic:
⟨fun h ↦ of_map F h, fun h ↦ h.map F⟩

Premises used: CategoryTheory.Square.IsPullback.of_map, CategoryTheory.Square.IsPullback.map, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
h : sq.IsPushout
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimit (span sq.f₁₂ sq.f₁₃) F
⊢ (sq.map F).IsPushout

Tactic:
Square.IsPushout.mk _ (isColimitPushoutCoconeMapOfIsColimit F sq.fac h.isColimit)

Premises used: CategoryTheory.Square.IsPushout.mk, CategoryTheory.Limits.isColimitPushoutCoconeMapOfIsColimit, CategoryTheory.Square.fac, CategoryTheory.Square.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : ReflectsColimit (span sq.f₁₂ sq.f₁₃) F
h : (sq.map F).IsPushout
⊢ sq.IsPushout

Tactic:
CategoryTheory.IsPushout.of_map F sq.fac h

Premises used: CategoryTheory.Square.fac, CategoryTheory.Square.IsPushout, CategoryTheory.IsPushout.of_map
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimit (span sq.f₁₂ sq.f₁₃) F
inst_3 : ReflectsColimit (span sq.f₁₂ sq.f₁₃) F
⊢ (sq.map F).IsPushout ↔ sq.IsPushout

Tactic:
⟨fun h ↦ of_map F h, fun h ↦ h.map F⟩

Premises used: CategoryTheory.Square.IsPushout.of_map, Iff.intro, CategoryTheory.Square.IsPushout.map