awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
simp : Eq (α := W ⟶ pushout f g) (h ≫ f ≫ pushout.inl f g) (h ≫ g ≫ pushout.inr f g)
⊢ Eq (α := W ⟶ pushout f g) ((h ≫ f) ≫ pushout.inl f g) ((h ≫ g) ≫ pushout.inr f g)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
rw : Eq (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (g ≫ pushout.inr f g)
⊢ Eq (α := W ⟶ pushout f g) (h ≫ f ≫ pushout.inl f g) (h ≫ g ≫ pushout.inr f g)

Tactic:
rw [cancel_epi]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
⊢ Eq (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (g ≫ pushout.inr f g)

Tactic:
pushout.condition

Premises used: CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
inst_2 : HasPushout f g
⊢ Eq (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (g ≫ pushout.inr f g)

Tactic:
exact pushout.condition

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

Tactic:
⟨⟨⟨_, pushoutIsPushoutOfEpiComp f g h⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
⊢ HasPushout h (h ≫ f)

Tactic:
simpa only [Category.comp_id] using hasPushout_of_epi_comp (𝟙 X) f h

Premises used: CategoryTheory.Limits.hasPushout_of_epi_comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
⊢ IsIso (Y := colimit (span (h ≫ 𝟙 X) (h ≫ f))) (colimit.ι (span (h ≫ 𝟙 X) (h ≫ f)) WalkingSpan.right)

Tactic:
(congrArg IsIso
          (show pushout.inr _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp (𝟙 _) f h⟩
              WalkingSpan.right)).mp
      inferInstance

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.IsIso, congrArg, CategoryTheory.CategoryStruct.id, inferInstance, Eq.mp, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp._proof_1, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp, CategoryTheory.Limits.pushout.inl, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
h₁ : h = h ≫ 𝟙 X
h₂ :
  Z = (span (h ≫ 𝟙 X) (h ≫ f)).obj WalkingSpan.right →
    pushout h (h ≫ f) = colimit (span (h ≫ 𝟙 X) (h ≫ f)) → h = h ≫ 𝟙 X
⊢ IsIso (Y := pushout h (h ≫ f)) (pushout.inr h (h ≫ f))

Tactic:
convert!
    (congrArg IsIso
          (show pushout.inr _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp (𝟙 _) f h⟩
              WalkingSpan.right)).mp
      inferInstance

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.IsIso, congrArg, CategoryTheory.CategoryStruct.id, inferInstance, Eq.mp, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp._proof_1, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp, CategoryTheory.Limits.pushout.inl, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
⊢ h = h ≫ 𝟙 X

Tactic:
apply (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
e_3 : Z = (span (h ≫ 𝟙 X) (h ≫ f)).obj WalkingSpan.right
e_4 : pushout h (h ≫ f) = colimit (span (h ≫ 𝟙 X) (h ≫ f))
⊢ h = h ≫ 𝟙 X

Tactic:
apply (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
⊢ HasPushout (h ≫ f) h

Tactic:
simpa only [Category.comp_id] using hasPushout_of_epi_comp f (𝟙 X) h

Premises used: CategoryTheory.Limits.hasPushout_of_epi_comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
⊢ IsIso (Y := colimit (span (h ≫ f) (h ≫ 𝟙 X))) (colimit.ι (span (h ≫ f) (h ≫ 𝟙 X)) WalkingSpan.left)

Tactic:
(congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩
              WalkingSpan.left)).mp
      inferInstance

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.IsIso, congrArg, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.CategoryStruct.id, inferInstance, Eq.mp, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp._proof_1, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp, CategoryTheory.Limits.pushout.inl, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
h₁ : h = h ≫ 𝟙 X
h₂ :
  Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left → pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X)) → h = h ≫ 𝟙 X
⊢ IsIso (Y := pushout (h ≫ f) h) (pushout.inl (h ≫ f) h)

Tactic:
convert!
    (congrArg IsIso
          (show pushout.inl _ _ ≫ _ = _ from
            colimit.isoColimitCocone_ι_inv ⟨_, pushoutIsPushoutOfEpiComp f (𝟙 _) h⟩
              WalkingSpan.left)).mp
      inferInstance

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.IsIso, congrArg, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.CategoryStruct.id, inferInstance, Eq.mp, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp._proof_1, CategoryTheory.Limits.pushoutIsPushoutOfEpiComp, CategoryTheory.Limits.pushout.inl, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.pushout.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
⊢ h = h ≫ 𝟙 X

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
⊢ h = h ≫ 𝟙 X

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
e_3 : Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left
e_4 : pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X))
⊢ h = h ≫ 𝟙 X

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f_1 : X ⟶ Z
h : W ⟶ X
inst_1 : Epi h
f : X ⟶ Y
e_3 : Y = (span (h ≫ f) (h ≫ 𝟙 X)).obj WalkingSpan.left
e_4 : pushout (h ≫ f) h = colimit (span (h ≫ f) (h ≫ 𝟙 X))
⊢ h = h ≫ 𝟙 X

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
⊢ HasPushout f f

Tactic:
⟨⟨⟨_, PushoutCocone.isColimitMkIdId f⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.PushoutCocone.isColimitMkIdId
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
⊢ t.inl = t.inr

Tactic:
(cancel_epi f).1 t.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
⊢ Eq (α := Y ⟶ pushout f f) (pushout.inl f f) (pushout.inr f f)

Tactic:
PushoutCocone.inl_eq_inr_of_epi_eq (getColimitCocone (span f f)).cocone

Premises used: CategoryTheory.Limits.ColimitCocone.cocone, CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq, CategoryTheory.Limits.colimit, CategoryTheory.Limits.span, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h₀ :
  CategoryStruct.comp (Y := pushout f f) (pushout.inl f f) (Iso.hom (pushoutSymmetry f f)) =
    pushout.inl f f ≫ 𝟙 (pushout f f)
h₁ :
  CategoryStruct.comp (Y := pushout f f) (pushout.inr f f) (Iso.hom (pushoutSymmetry f f)) =
    pushout.inr f f ≫ 𝟙 (pushout f f)
⊢ Iso.hom (pushoutSymmetry f f) = 𝟙 (pushout f f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
⊢ CategoryStruct.comp (Y := pushout f f) (pushout.inl f f) (Iso.hom (pushoutSymmetry f f)) =
    pushout.inl f f ≫ 𝟙 (pushout f f)

Tactic:
simp [inl_eq_inr_of_epi_eq]

Premises used: CategoryTheory.Limits.inl_eq_inr_of_epi_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
⊢ CategoryStruct.comp (Y := pushout f f) (pushout.inr f f) (Iso.hom (pushoutSymmetry f f)) =
    pushout.inr f f ≫ 𝟙 (pushout f f)

Tactic:
simp [inl_eq_inr_of_epi_eq]

Premises used: CategoryTheory.Limits.inl_eq_inr_of_epi_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
refine : IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt
⊢ IsIso t.inl

Tactic:
refine ⟨⟨PushoutCocone.IsColimit.desc ht (𝟙 _) (𝟙 _) (by simp), by simp, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
h₀ : t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt
h₁ : t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inr ≫ 𝟙 t.pt
⊢ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = 𝟙 t.pt

Tactic:
apply PushoutCocone.IsColimit.hom_ext ht

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inr ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inr ≫ 𝟙 t.pt

Tactic:
simp [inl_eq_inr_of_epi_eq]

Premises used: CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ IsIso t.inr

Tactic:
t.inl_eq_inr_of_epi_eq ▸ t.isIso_inl_of_epi_of_isColimit ht

Premises used: CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq, Eq.rec, CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
⊢ IsIso (Y := pushout f f) (pushout.inl f f)

Tactic:
PushoutCocone.isIso_inl_of_epi_of_isColimit (getColimitCocone (span f f)).isColimit

Premises used: CategoryTheory.Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
⊢ IsIso (Y := pushout f f) (pushout.inr f f)

Tactic:
PushoutCocone.isIso_inr_of_epi_of_isColimit (getColimitCocone (span f f)).isColimit

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit, CategoryTheory.Limits.colimit.ι
-- 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
rw : t₁.snd ≫ i₂ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃
rw₁ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.snd ≫ i₃
rw₂ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.fst ≫ g₂
rw₃ rw₄ : t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ i₂ ≫ g₂
⊢ t₁.fst ≫ g₁ ≫ g₂ = (t₁.snd ≫ t₂.snd) ≫ i₃

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₃ 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₁
create :
  (s : PullbackCone (g₁ ≫ g₂) i₃) →
    { l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt //
      l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
        l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
            m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }
⊢ IsLimit (t₂.pasteHoriz t₁ hi₂)

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₁
s : PullbackCone (g₁ ≫ g₂) i₃
rw : (s.fst ≫ g₁) ≫ g₂ = s.fst ≫ g₁ ≫ g₂
rw₁ rw₂ : s.fst ≫ g₁ ≫ g₂ = s.fst ≫ g₁ ≫ g₂
⊢ (s.fst ≫ g₁) ≫ g₂ = s.snd ≫ i₃

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

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

Tactic:
obtain ⟨l₂, hl₂, hl₂'⟩ := PullbackCone.IsLimit.lift' H (s.fst ≫ g₁) s.snd
    (by rw [← s.condition, Category.assoc])

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.lift', CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.PullbackCone.snd
-- 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
rw : l₂ ≫ t₂.fst = l₂ ≫ i₂
rw₁ rw₂ : l₂ ≫ t₂.fst = l₂ ≫ t₂.fst
⊢ s.fst ≫ g₁ = l₂ ≫ i₂

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

Tactic:
obtain ⟨l₁, hl₁, hl₁'⟩ := PullbackCone.IsLimit.lift' H' s.fst l₂ (by rw [← hl₂, hi₂])

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.lift'
-- 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₂
⊢ l₁ ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd

Tactic:
simp [reassoc_of% hl₁', 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₁
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₂
create :
  ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
    m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l₁
⊢ { l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt //
    l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst ∧
      l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
          m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l }

Tactic:
refine ⟨l₁, hl₁, by simp [reassoc_of% hl₁', 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₁
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₁.fst = l₁ ≫ t₁.fst

Tactic:
simpa [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₁
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
create : m ≫ t₁.snd = l₁ ≫ t₁.snd
⊢ m = l₁

Tactic:
apply PullbackCone.IsLimit.hom_ext H' (by simpa [hl₁] using hm₁)

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₁
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
create : (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : (m ≫ t₁.snd) ≫ t₂.snd = (l₁ ≫ t₁.snd) ≫ t₂.snd
⊢ m ≫ t₁.snd = l₁ ≫ t₁.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₁
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₁.fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
create : m ≫ t₁.snd ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst
create₁ : m ≫ t₁.snd ≫ i₂ = (l₁ ≫ t₁.snd) ≫ i₂
create₂ : m ≫ t₁.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₃ : s.fst ≫ g₁ = (l₁ ≫ t₁.snd) ≫ i₂
create₄ : s.fst ≫ g₁ = l₂ ≫ i₂
create₅ : s.fst ≫ g₁ = l₂ ≫ t₂.fst
create₆ create₇ : s.fst ≫ g₁ = s.fst ≫ g₁
⊢ (m ≫ t₁.snd) ≫ t₂.fst = (l₁ ≫ t₁.snd) ≫ t₂.fst

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition