awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ (m ≫ t₁.snd) ≫ t₂.snd = (l₁ ≫ t₁.snd) ≫ t₂.snd

Tactic:
simpa [hl₁', hl₂'] using hm₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
create :
  (s : PullbackCone g₁ i₂) →
    { l : s.pt ⟶ t₁.pt //
      l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
⊢ IsLimit t₁

Tactic:
apply PullbackCone.isLimitAux'

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
rw : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.snd ≫ i₃
rw₁ : s.fst ≫ g₁ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
rw₂ : s.snd ≫ i₂ ≫ g₂ = s.snd ≫ t₂.fst ≫ g₂
rw₃ rw₄ : s.snd ≫ i₂ ≫ g₂ = s.snd ≫ i₂ ≫ g₂
⊢ s.fst ≫ g₁ ≫ g₂ = (s.snd ≫ t₂.snd) ≫ i₃

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
create :
  (l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt) →
    (hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst) →
      (hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd) →
        { l : s.pt ⟶ t₁.pt //
          l ≫ t₁.fst = s.fst ∧
            l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }
⊢ { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }

Tactic:
obtain ⟨l, hl, hl'⟩ := PullbackCone.IsLimit.lift' H' s.fst (s.snd ≫ f₂)
    (by rw [Category.assoc, ← t₂.condition, reassoc_of% s.condition, ← hi₂])
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
create : l ≫ t₁.snd = s.snd
create₁ : ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l
⊢ { l : s.pt ⟶ t₁.pt //
    l ≫ t₁.fst = s.fst ∧ l ≫ t₁.snd = s.snd ∧ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l }

Tactic:
refine ⟨l, hl, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
create : (l ≫ t₁.snd) ≫ t₂.fst = s.snd ≫ t₂.fst
create₁ : (l ≫ t₁.snd) ≫ t₂.snd = s.snd ≫ t₂.snd
⊢ l ≫ t₁.snd = s.snd

Tactic:
apply PullbackCone.IsLimit.hom_ext H

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ (l ≫ t₁.snd) ≫ t₂.fst = s.snd ≫ t₂.fst

Tactic:
simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ (l ≫ t₁.snd) ≫ t₂.snd = s.snd ≫ t₂.snd

Tactic:
simpa using hl'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
create : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = l ≫ (t₂.pasteHoriz t₁ hi₂).fst
create₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = l ≫ (t₂.pasteHoriz t₁ hi₂).snd
⊢ m = l

Tactic:
apply PullbackCone.IsLimit.hom_ext H'

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Goal:
C : Type u
inst : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m ≫ (t₂.pasteHoriz t₁ hi₂).fst = l ≫ (t₂.pasteHoriz t₁ hi₂).fst

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₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m ≫ (t₂.pasteHoriz t₁ hi₂).snd = l ≫ (t₂.pasteHoriz t₁ hi₂).snd

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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
rw : (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
rw₁ : t₂.fst ≫ t₁.fst ≫ i₁ = t₂.fst ≫ i₂ ≫ f₁
rw₂ : t₂.fst ≫ t₁.snd ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁
rw₃ rw₄ : t₂.fst ≫ i₂ ≫ f₁ = t₂.fst ≫ i₂ ≫ f₁
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
⊢ (t₁.pasteVert t₂ hi₂).flip.fst =
    Iso.hom (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) ≫ (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂).fst

Tactic:
simp
-- 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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
⊢ (t₁.pasteVert t₂ hi₂).flip.snd =
    Iso.hom (Iso.refl (t₁.pasteVert t₂ hi₂).flip.pt) ≫ (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂).snd

Tactic:
simp
-- 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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
H₁ : IsLimit t₁
H₂ : IsLimit t₂
⊢ IsLimit (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂)

Tactic:
exact pasteHorizIsPullback hi₂ (PullbackCone.flipIsLimit H₁) (PullbackCone.flipIsLimit H₂)

Premises used: CategoryTheory.Limits.PullbackCone.flipIsLimit, CategoryTheory.Limits.pasteHorizIsPullback
-- 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
rw : f₁ ≫ t₁.inr ≫ t₂.inl = (f₁ ≫ f₂) ≫ t₂.inr
rw₁ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ f₂ ≫ t₂.inr
rw₂ : f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
rw₃ rw₄ : f₁ ≫ i₂ ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
⊢ i₁ ≫ t₁.inl ≫ t₂.inl = (f₁ ≫ f₂) ≫ 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
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₂
create :
  (s : PushoutCocone i₁ (f₁ ≫ f₂)) →
    { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
      (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
        (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
          ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
            (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
⊢ IsColimit (t₁.pasteHoriz t₂ hi₂)

Tactic:
apply PushoutCocone.isColimitAux'

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux'
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
rw : (f₁ ≫ f₂) ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
rw₁ rw₂ : f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
⊢ i₁ ≫ s.inl = f₁ ≫ f₂ ≫ s.inr

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

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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
create :
  (l₁ : t₁.pt ⟶ s.pt) →
    (hl₁ : t₁.inl ≫ l₁ = s.inl) →
      (hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr) →
        { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
          (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
            (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
              ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
                (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }

Tactic:
obtain ⟨l₁, hl₁, hl₁'⟩ := PushoutCocone.IsColimit.desc' H s.inl (f₂ ≫ s.inr)
    (by rw [s.condition, Category.assoc])

Premises used: CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl, CategoryTheory.Limits.PushoutCocone.IsColimit.desc', CategoryTheory.CategoryStruct.comp
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
rw : «i₂» ≫ l₁ = t₁.inr ≫ l₁
rw₁ rw₂ : t₁.inr ≫ l₁ = t₁.inr ≫ l₁
⊢ «i₂» ≫ l₁ = f₂ ≫ s.inr

Tactic:
rw [← hl₁', hi₂]
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
create :
  (l₂ : t₂.pt ⟶ s.pt) →
    (hl₂ : t₂.inl ≫ l₂ = l₁) →
      (hl₂' : t₂.inr ≫ l₂ = s.inr) →
        { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
          (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
            (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
              ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
                (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }

Tactic:
obtain ⟨l₂, hl₂, hl₂'⟩ := PushoutCocone.IsColimit.desc' H' l₁ s.inr (by rw [← hl₁', hi₂])

Premises used: CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.IsColimit.desc'
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ l₂ = s.inl

Tactic:
simp [hl₂, hl₁]
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
create :
  ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
    (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l₂
⊢ { l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt //
    (t₁.pasteHoriz t₂ hi₂).inl ≫ l = s.inl ∧
      (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr ∧
        ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
          (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l }

Tactic:
refine ⟨l₂, by simp [hl₂, hl₁], hl₂', ?_⟩
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inr ≫ m = t₂.inr ≫ l₂

Tactic:
simpa [hl₂'] using hm₂
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
apply : t₂.inl ≫ m = t₂.inl ≫ l₂
⊢ m = l₂

Tactic:
apply PushoutCocone.IsColimit.hom_ext H' _ (by simpa [hl₂'] using hm₂)

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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₁.inl ≫ t₂.inl ≫ m = s.inl

Tactic:
simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hm₁ hm₂

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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₀ : t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂
h₁ : t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂
⊢ t₂.inl ≫ m = t₂.inl ≫ 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₀ : s.inl = t₁.inl ≫ t₂.inl ≫ l₂
h₁ : t₁.inl ≫ l₁ = t₁.inl ≫ t₂.inl ≫ l₂
h₂ h₃ : t₁.inl ≫ l₁ = t₁.inl ≫ l₁
⊢ t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l₂

Tactic:
rw [hm₁, ← hl₁, hl₂]
-- 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₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₂ : t₂.inr ≫ m = s.inr
hm₁ : t₁.inl ≫ t₂.inl ≫ m = s.inl
h₁ : «i₂» ≫ t₂.inl ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₂ : f₂ ≫ t₂.inr ≫ m = «i₂» ≫ t₂.inl ≫ l₂
h₃ : f₂ ≫ t₂.inr ≫ m = f₂ ≫ t₂.inr ≫ l₂
h₄ : f₂ ≫ s.inr = f₂ ≫ t₂.inr ≫ l₂
h₅ h₆ : f₂ ≫ s.inr = f₂ ≫ s.inr
⊢ t₁.inr ≫ t₂.inl ≫ m = t₁.inr ≫ t₂.inl ≫ l₂

Tactic:
rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']

Premises used: 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₂)
create :
  (s : PushoutCocone «i₂» f₂) →
    { l : t₂.pt ⟶ s.pt //
      t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
⊢ IsColimit t₂

Tactic:
apply PushoutCocone.isColimitAux'

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux'
-- 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₂
rw : f₁ ≫ t₁.inr ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
rw₁ : f₁ ≫ «i₂» ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr
rw₂ : f₁ ≫ f₂ ≫ s.inr = (f₁ ≫ f₂) ≫ s.inr
rw₃ rw₄ : f₁ ≫ f₂ ≫ s.inr = f₁ ≫ f₂ ≫ s.inr
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr

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

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₂
create :
  (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) →
        { l : t₂.pt ⟶ s.pt //
          t₂.inl ≫ l = s.inl ∧
            t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }
⊢ { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }

Tactic:
obtain ⟨l, hl, hl'⟩ := PushoutCocone.IsColimit.desc' H' (g₁ ≫ s.inl) s.inr
    (by rw [reassoc_of% t₁.condition, ← hi₂, s.condition, Category.assoc])
-- 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
create : t₂.inl ≫ l = s.inl
create₁ : ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l
⊢ { l : t₂.pt ⟶ s.pt //
    t₂.inl ≫ l = s.inl ∧ t₂.inr ≫ l = s.inr ∧ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l }

Tactic:
refine ⟨l, ?_, hl', ?_⟩