awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
apply :
  IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
    (Cofan.mk (G.obj (sigmaObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Sigma.ι f j))
⊢ IsColimit (G.mapCocone (Cofan.mk (sigmaObj.{w, v₁, u₁} f) (Sigma.ι f)))

Tactic:
apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _

Premises used: CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
⊢ IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
    (Cofan.mk (G.obj (sigmaObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Sigma.ι f j))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _
    (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.IsColimit.ofPointIso, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
j : J
⊢ Eq (α := G.obj (f j) ⟶ sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b))
    (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v₁, u₁} f)) (G.map (Sigma.ι f j)) (inv (sigmaComparison G f)))
    (Sigma.ι.{w, v₂, u₂} (C := D) (fun (x : J) ↦ G.obj (f x)) j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : PreservesColimit (Discrete.functor f) G
⊢ Eq (α := (sigmaObj.{w, v₂, u₂} fun (j : J) ↦ G.obj (f j)) ⟶ G.obj (sigmaObj.{w, v₁, u₁} f)) (Iso.inv (iso G f))
    (sigmaComparison G f)

Tactic:
rfl

Premises used: CategoryTheory.Limits.sigmaComparison, CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : PreservesColimit (Discrete.functor f) G
⊢ IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (Iso.inv (PreservesCoproduct.iso G f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
J : Type w
f : J → C
I : Type w
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (Discrete I) F
⊢ PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (Discrete I)ᵒᵖ F

Tactic:
preservesColimitsOfShape_of_equiv (Discrete.opposite I).symm F

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ G.map c.fst ≫ G.map f = G.map c.snd ≫ G.map g

Tactic:
simpa using G.congr_map c.condition

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Functor.congr_map
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 :
  fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).fst
refine_2 :
  snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).snd
⊢ (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c) ≅ c.map G

Tactic:
refine PullbackCone.ext (Iso.refl _) ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.PullbackCone.ext
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 :
  ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
      (c.map G).π.app WalkingCospan.left
⊢ fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).fst

Tactic:
dsimp only [fst]

Premises used: CategoryTheory.Limits.PullbackCone.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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
      (c.map G).π.app WalkingCospan.left

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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_2 :
  ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
      (c.map G).π.app WalkingCospan.right
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).snd

Tactic:
dsimp only [snd]

Premises used: CategoryTheory.Limits.PullbackCone.snd
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.right =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
      (c.map G).π.app WalkingCospan.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
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

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
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
rw : G.map (h ≫ f) = G.map k ≫ G.map g
rw₁ : G.map (h ≫ f) = G.map (k ≫ g)
rw₂ rw₃ : G.map (k ≫ g) = G.map (k ≫ g)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
rw [← G.map_comp, ← 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
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : ReflectsLimit (cospan f g) G
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

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
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj Z) (G.map (pullback.fst f g) ≫ G.map f) (G.map (pullback.snd f g) ≫ G.map g)

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

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
apply : IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
⊢ IsLimit (G.mapCone c)

Tactic:
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
apply : IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯)
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))

Tactic:
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm

Premises used: CategoryTheory.Limits.PullbackCone.isoMk, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯).flip
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯)

Tactic:
apply PullbackCone.isLimitOfFlip

Premises used: CategoryTheory.Limits.PullbackCone.isLimitOfFlip
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯))
apply :
  c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯).flip

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).toFun

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯)
ht₁ : PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G
⊢ IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯))

Tactic:
refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯).flip
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯)

Tactic:
apply PullbackCone.isLimitOfFlip

Premises used: CategoryTheory.Limits.PullbackCone.isLimitOfFlip
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
apply : IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯).flip

Tactic:
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)

Premises used: CategoryTheory.Limits.PullbackCone.isoMk, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)

Tactic:
exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : PreservesLimit (cospan f g) G
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G

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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan f g) 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 ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl

Tactic:
(c.π.naturality WalkingCospan.Hom.inr).symm.trans
          (c.π.naturality WalkingCospan.Hom.inl :)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.WalkingCospan.Hom.inr, Eq.symm, Eq.trans
-- 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 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl

Tactic:
exact
        (c.π.naturality WalkingCospan.Hom.inr).symm.trans
          (c.π.naturality WalkingCospan.Hom.inl :)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.WalkingCospan.Hom.inr, Eq.symm, Eq.trans
-- 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 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
⊢ HasPullback (G.map f) (G.map g)

Tactic:
⟨⟨⟨_, isLimitPullbackConeMapOfIsLimit G _ (pullbackIsPullback _ _)⟩⟩⟩

Premises used: CategoryTheory.Limits.pullbackIsPullback, Nonempty.intro, CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- 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 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
inst_4 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ pullback (G.map f) (G.map g)) (Iso.hom (iso G f g)) (pullbackComparison G f g)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.pullbackComparison, 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
inst_4 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj X)
    (CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (Iso.hom (iso G f g)) (pullback.fst (G.map f) (G.map g)))
    (G.map (pullback.fst f g))

Tactic:
simp [PreservesPullback.iso]

Premises used: CategoryTheory.Limits.PreservesPullback.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 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
inst_4 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := G.obj (pullback f g) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (Iso.hom (iso G f g)) (pullback.snd (G.map f) (G.map g)))
    (G.map (pullback.snd f g))

Tactic:
simp [PreservesPullback.iso]

Premises used: CategoryTheory.Limits.PreservesPullback.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 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
inst_4 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := pullback (G.map f) (G.map g) ⟶ G.obj X)
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (Iso.inv (iso G f g)) (G.map (pullback.fst f g)))
    (pullback.fst (G.map f) (G.map g))

Tactic:
simp [PreservesPullback.iso, Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.PreservesPullback.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 : PreservesLimit (cospan f g) G
inst_3 : HasPullback f g
inst_4 : HasPullback (G.map f) (G.map g)
⊢ Eq (α := pullback (G.map f) (G.map g) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (Iso.inv (iso G f g)) (G.map (pullback.snd f g)))
    (pullback.snd (G.map f) (G.map g))

Tactic:
simp [PreservesPullback.iso, Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.PreservesPullback.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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ G.map f ≫ G.map c.inl = G.map g ≫ G.map c.inr

Tactic:
simpa using G.congr_map c.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Functor.congr_map
-- 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_1 :
  inl ((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).inl
refine_2 :
  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
⊢ (Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c) ≅ c.map G

Tactic:
refine PushoutCocone.ext (Iso.refl _) ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.PushoutCocone.ext
-- 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_1 :
  ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).ι.app WalkingSpan.left
⊢ inl ((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).inl

Tactic:
dsimp only [inl]

Premises used: CategoryTheory.Limits.PushoutCocone.inl
-- 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.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).ι.app WalkingSpan.left

Tactic:
simp