awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← comminl, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← comminr, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y : C
inl inr : X ⟶ P
f : Y ⟶ X
h : IsPushout f f inl inr
inst : Epi f
⊢ IsIso inl

Tactic:
h.cocone.isIso_inl_of_epi_of_isColimit h.isColimit

Premises used: CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
P X Y : C
inl inr : X ⟶ P
f : Y ⟶ X
h : IsPushout f f inl inr
inst : Epi f
⊢ IsIso inr

Tactic:
h.cocone.isIso_inr_of_epi_of_isColimit h.isColimit

Premises used: CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
left_cancellation : ∀ {Z : C} (g h : P ⟶ Z), inl ≫ g = inl ≫ h → g = h
⊢ Epi inl

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ inr ≫ fst' = inr ≫ snd'

Tactic:
simp [← cancel_epi g, ← h.w_assoc, heq]

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ fst' = snd'

Tactic:
exact h.hom_ext heq (by simp [← cancel_epi g, ← h.w_assoc, heq])

Premises used: CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi f
⊢ Epi inr

Tactic:
h.flip.epi_inl_of_epi

Premises used: CategoryTheory.IsPushout.epi_inl_of_epi, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso g
⊢ HasPushout f g

Tactic:
have := h.hasPushout
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso g
this : HasPushout f g
rw : IsIso (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout))
⊢ IsIso inl

Tactic:
rw [← h.inl_isoPushout_inv]

Premises used: CategoryTheory.IsPushout.inl_isoPushout_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso g
this : HasPushout f g
⊢ IsIso (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : IsIso f
⊢ IsIso inr

Tactic:
h.flip.isIso_inl_of_isIso

Premises used: CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.isIso_inl_of_isIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
t : IsPushout h₂₁ v₂₁ v₂₂ h₃₁
⊢ IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁

Tactic:
of_isColimit (pasteHorizIsPushout rfl s.isColimit t.isColimit)

Premises used: CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.IsPushout.isColimit, CategoryTheory.IsPushout.of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
t : IsPushout h₁₂ v₁₂ v₁₃ h₂₂
⊢ IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)

Tactic:
(paste_vert s.flip t.flip).flip

Premises used: CategoryTheory.IsPushout.paste_vert, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁
p : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ IsPushout h₂₁ v₂₁ v₂₂ h₃₁

Tactic:
of_isColimit <| rightSquareIsPushout
    (PushoutCocone.mk _ _ p) (cocone_inr _) t.isColimit s.isColimit

Premises used: CategoryTheory.IsPushout.cocone_inr, CategoryTheory.Limits.rightSquareIsPushout, CategoryTheory.IsPushout.isColimit, CategoryTheory.IsPushout.of_isColimit, CategoryTheory.Limits.PushoutCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
p : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ IsPushout h₁₂ v₁₂ v₁₃ h₂₂

Tactic:
(of_top s.flip p.symm t.flip).flip

Premises used: CategoryTheory.IsPushout.of_top, CategoryTheory.IsPushout.flip, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₂₁ : X₂₁ ⟶ X₃₁
v₂₂ : X₂₂ ⟶ X₃₂
s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
e : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁
⊢ IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ ↔ IsPushout h₂₁ v₂₁ v₂₂ h₃₁

Tactic:
⟨fun h => h.of_top e s, s.paste_vert⟩

Premises used: CategoryTheory.IsPushout.of_top, CategoryTheory.IsPushout.paste_vert, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
e : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂
⊢ IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) ↔ IsPushout h₁₂ v₁₂ v₁₃ h₂₂

Tactic:
⟨fun h => h.of_left e s, s.paste_horiz⟩

Premises used: CategoryTheory.IsPushout.of_left, CategoryTheory.IsPushout.paste_horiz, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
rw : (v₁₁ ≫ v₂₁) ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
rw₁ rw₂ : v₁₁ ≫ v₂₁ ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
rw [s.w, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ IsPushout h₂₁ v₂₁ (t.desc v₁₃ (v₂₁ ≫ h₃₁) ⋯) h₃₁

Tactic:
of_top ((t.inl_desc _ _ _).symm ▸ s) (t.inr_desc _ _ _) t

Premises used: CategoryTheory.IsPushout.of_top, CategoryTheory.IsPushout.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
rw : (h₁₁ ≫ h₁₂) ≫ v₁₃ = v₁₁ ≫ h₂₃
rw₁ rw₂ : v₁₁ ≫ h₂₃ = v₁₁ ≫ h₂₃
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃

Tactic:
rw [← Category.assoc, s.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₂ ≫ v₁₃ = v₁₂ ≫ t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯

Tactic:
simp only [inl_desc]

Premises used: CategoryTheory.IsPushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : Epi f
inst_2 : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ (fun (s : PushoutCocone f g) ↦ inv inr ≫ s.inr) s = s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : Epi f
inst_2 : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt),
    inl ≫ m = s.inl → inr ≫ m = s.inr → m = (fun (s : PushoutCocone f g) ↦ inv inr ≫ s.inr) s

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : Epi f
inst_2 : IsIso inr
sq : CommSq f g inl inr
_ : ∀ (s : PushoutCocone f g), inl ≫ (fun (s : PushoutCocone f g) ↦ inv inr ≫ s.inr) s = s.inl
⊢ IsColimit sq.cocone

Tactic:
refine
        PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
          (by simp) (by simp)

Premises used: CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.IsColimit.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : Epi f
inst_2 : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun (s : PushoutCocone f g) ↦ inv inr ≫ s.inr) s = s.inl

Tactic:
simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.CommSq.w_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : IsIso f
inst_2 : IsIso inr
sq : CommSq f g inl inr
⊢ IsPushout f g inl inr

Tactic:
of_horiz_isIso_epi sq

Premises used: CategoryTheory.IsPushout.of_horiz_isIso_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : Epi g
inst_2 : IsIso inl
sq : CommSq f g inl inr
⊢ IsPushout f g inl inr

Tactic:
(of_horiz_isIso_epi sq.flip).flip

Premises used: CategoryTheory.CommSq.flip, CategoryTheory.IsPushout.of_horiz_isIso_epi, CategoryTheory.IsPushout.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_1 : IsIso g
inst_2 : IsIso inl
sq : CommSq f g inl inr
⊢ IsPushout f g inl inr

Tactic:
of_vert_isIso_epi sq

Premises used: CategoryTheory.IsPushout.of_vert_isIso_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
f : Z ⟶ X
⊢ 𝟙 Z ≫ f = f ≫ 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
f : Z ⟶ X
⊢ f ≫ 𝟙 X = 𝟙 Z ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp only [Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
⊢ Eq (α := A ⟶ coprod.{v₁, u₁} B X) (CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inl (coprod.map f (𝟙 X)))
    (f ≫ coprod.inl)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
refine_1 :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl
refine_2 :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inr
refine_3 :
  ∀
    {m :
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
        s.pt},
    PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m = s.inl →
      PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m = s.inr →
        m = coprod.desc s.inr (coprod.inr ≫ s.inl)
⊢ { l :
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
      s.pt //
    PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inr ∧
        ∀
          {m :
            Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
                (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
              s.pt},
          PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
              s.inl →
            PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
                s.inr →
              m = l }

Tactic:
refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
refine_1 :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inl
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
    coprod.inl ≫ s.inl
refine_1₁ :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inr
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
    coprod.inr ≫ s.inl
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
⊢ CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inl
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
    coprod.inl ≫ s.inl

Tactic:
simp [PushoutCocone.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
⊢ CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inr
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
    coprod.inr ≫ s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
m :
  Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
      (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
    s.pt
h₁ : PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m = s.inl
h₂ : PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m = s.inr
refine_3 : m = coprod.desc s.inr (coprod.inr ≫ s.inl)
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
dsimp at m h₁ h₂ ⊢
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
m : coprod.{v₁, u₁} B X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
refine_3 :
  coprod.inl ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inl (coprod.desc s.inr (coprod.inr ≫ s.inl))
refine_3₁ :
  coprod.inr ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inr (coprod.desc s.inr (coprod.inr ≫ s.inl))
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
m : coprod.{v₁, u₁} B X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inl ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inl (coprod.desc s.inr (coprod.inr ≫ s.inl))

Tactic:
simpa using h₂