awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl

Tactic:
simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hl hl'

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.mk_ι_app, CategoryTheory.Limits.PushoutCocone.mk_pt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
⊢ t₂.inl ≫ l = s.inl

Tactic:
apply PushoutCocone.IsColimit.hom_ext H hl

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
create₂ : (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
create₃ : (f₂ ≫ t₂.inr) ≫ l = f₂ ≫ s.inr
create₄ : f₂ ≫ t₂.inr ≫ l = f₂ ≫ s.inr
create₅ create₆ : f₂ ≫ s.inr = f₂ ≫ s.inr
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl

Tactic:
rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
create : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l
create₁ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l
⊢ m = l

Tactic:
apply PushoutCocone.IsColimit.hom_ext H'

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l

Tactic:
simpa [← hm₁] using hl.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l

Tactic:
simpa [← hm₂] using hl'.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁_1 : PushoutCocone g₂ i₃
i₂_1 : Y₂ ⟶ t₁_1.pt
t₂_1 : PushoutCocone g₁ i₂_1
hi₂_1 : i₂_1 = t₁_1.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
rw : (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
rw₁ : g₂ ≫ g₁ ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
rw₂ : g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ t₁.inl ≫ t₂.inr
rw₃ rw₄ : g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ i₂ ≫ t₂.inr
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr

Tactic:
rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
⊢ (t₁.pasteVert t₂ hi₂).flip.inl ≫ Iso.hom (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) =
    (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂).inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
⊢ (t₁.pasteVert t₂ hi₂).flip.inr ≫ Iso.hom (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) =
    (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂).inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
H₁ : IsColimit t₁
H₂ : IsColimit t₂
apply : IsColimit (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂)
⊢ IsColimit (t₁.pasteVert t₂ hi₂)

Tactic:
apply PushoutCocone.isColimitOfFlip <| IsColimit.ofIsoColimit _ (t₁.pasteVertFlip t₂ hi₂).symm

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.PushoutCocone.pasteVertFlip, CategoryTheory.Iso.symm, CategoryTheory.Limits.PushoutCocone.isColimitOfFlip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
H₁ : IsColimit t₁
H₂ : IsColimit t₂
⊢ IsColimit (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂)

Tactic:
exact pasteHorizIsPushout hi₂ (PushoutCocone.flipIsColimit H₁) (PushoutCocone.flipIsColimit H₂)

Premises used: CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.Limits.PushoutCocone.flipIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ HasPullback (f' ≫ f) g

Tactic:
HasLimit.mk {
    cone := (pullback.cone f g).pasteHoriz (pullback.cone f' (pullback.fst f g)) rfl
    isLimit := pasteHorizIsPullback rfl (pullback.isLimit f g)
      (pullback.isLimit f' (pullback.fst f g))
  }

Premises used: CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.pullback.fst, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.pasteHorizIsPullback, CategoryTheory.Limits.PullbackCone.pasteHoriz, rfl, CategoryTheory.Limits.pullback.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (Y := pullback f g) f' (pullback.fst f g) ⟶ W)
    (Iso.hom (pullbackRightPullbackFstIso f g f') ≫ pullback.fst (f' ≫ f) g) (pullback.fst f' (pullback.fst f g))

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (Y := pullback f g) f' (pullback.fst f g) ⟶ Y)
    (Iso.hom (pullbackRightPullbackFstIso f g f') ≫ pullback.snd (f' ≫ f) g)
    (pullback.snd f' (pullback.fst f g) ≫ pullback.snd f g)

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ W)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.fst f' (pullback.fst f g)) :
      pullback (f' ≫ f) g ⟶ W)
    (pullback.fst (f' ≫ f) g : pullback (f' ≫ f) g ⟶ W)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.snd f' (pullback.fst f g) ≫ pullback.snd f g) :
      pullback (f' ≫ f) g ⟶ Y)
    (pullback.snd (f' ≫ f) g : pullback (f' ≫ f) g ⟶ Y)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.cospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
rw :
  Eq (α := pullback (f' ≫ f) g ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.fst f' (pullback.fst f g) ≫ f') :
      pullback (f' ≫ f) g ⟶ X)
    (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.snd f' (pullback.fst f g) ≫ pullback.fst f g) :
      pullback (f' ≫ f) g ⟶ X)
    (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)

Tactic:
rw [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.fst f' (pullback.fst f g) ≫ f') :
      pullback (f' ≫ f) g ⟶ X)
    (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)

Tactic:
pullbackRightPullbackFstIso_inv_fst_assoc f g f' _

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.fst f' (pullback.fst f g) ≫ f') :
      pullback (f' ≫ f) g ⟶ X)
    (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)

Tactic:
exact pullbackRightPullbackFstIso_inv_fst_assoc f g f' _

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ HasPullback f (g' ≫ g)

Tactic:
HasLimit.mk {
    cone := (pullback.cone f g).pasteVert (pullback.cone (pullback.snd f g) g') rfl
    isLimit := pasteVertIsPullback rfl (pullback.isLimit f g)
      (pullback.isLimit (pullback.snd f g) g')
  }

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.PullbackCone.pasteVert, CategoryTheory.Limits.pasteVertIsPullback, CategoryTheory.Limits.LimitCone.mk, rfl, CategoryTheory.Limits.pullback.cone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback (X := pullback f g) (pullback.snd f g) g' ⟶ X)
    (Iso.hom (pullbackLeftPullbackSndIso f g g') ≫ pullback.fst f (g' ≫ g))
    (pullback.fst (pullback.snd f g) g' ≫ pullback.fst f g)

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback (X := pullback f g) (pullback.snd f g) g' ⟶ W)
    (Iso.hom (pullbackLeftPullbackSndIso f g g') ≫ pullback.snd f (g' ≫ g)) (pullback.snd (pullback.snd f g) g')

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback f (g' ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.fst (pullback.snd f g) g' ≫ pullback.fst f g) :
      pullback f (g' ≫ g) ⟶ X)
    (pullback.fst f (g' ≫ g) : pullback f (g' ≫ g) ⟶ X)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback f (g' ≫ g) ⟶ W)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.snd (pullback.snd f g) g') :
      pullback f (g' ≫ g) ⟶ W)
    (pullback.snd f (g' ≫ g) : pullback f (g' ≫ g) ⟶ W)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.cospan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
rw :
  Eq (α := pullback f (g' ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.snd (pullback.snd f g) g' ≫ g') :
      pullback f (g' ≫ g) ⟶ Y)
    (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)
⊢ Eq (α := pullback f (g' ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.fst (pullback.snd f g) g' ≫ pullback.snd f g) :
      pullback f (g' ≫ g) ⟶ Y)
    (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)

Tactic:
rw [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback f (g' ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.snd (pullback.snd f g) g' ≫ g') :
      pullback f (g' ≫ g) ⟶ Y)
    (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)

Tactic:
pullbackLeftPullbackSndIso_inv_snd_snd_assoc f g g' g'

Premises used: CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback f (g' ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.snd (pullback.snd f g) g' ≫ g') :
      pullback f (g' ≫ g) ⟶ Y)
    (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)

Tactic:
exact pullbackLeftPullbackSndIso_inv_snd_snd_assoc f g g' g'

Premises used: CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ HasPushout f (g ≫ g')

Tactic:
HasColimit.mk {
    cocone := (pushout.cocone f g).pasteHoriz (pushout.cocone (pushout.inr f g) g') rfl
    isColimit := pasteHorizIsPushout rfl (pushout.isColimit f g)
      (pushout.isColimit (pushout.inr f g) g')
  }

Premises used: CategoryTheory.Limits.PushoutCocone.pasteHoriz, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.Limits.pushout.isColimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushout.cocone, rfl, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := Y ⟶ pushout (Y := pushout f g) (pushout.inr f g) g')
    (pushout.inl f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
    (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g')

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := W ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr (pushout.inr f g) g')
        (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      W ⟶ pushout f (g ≫ g'))
    (pushout.inr f (g ≫ g') : W ⟶ pushout f (g ≫ g'))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom (pasteHorizIsPushout _ _ _) _ WalkingSpan.right

Premises used: CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.Limits.colimit, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := W ⟶ pushout (Y := pushout f g) (pushout.inr f g) g')
    (pushout.inr f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g')) (pushout.inr (pushout.inr f g) g')

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.right

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Y ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Y ⟶ pushout f (g ≫ g'))
    (pushout.inl f (g ≫ g') : Y ⟶ pushout f (g ≫ g'))
⊢ Eq (α := Y ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Y ⟶ pushout f (g ≫ g'))
    (pushout.inl f (g ≫ g') : Y ⟶ pushout f (g ≫ g'))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc