awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.inr ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inr (coprod.desc s.inr (coprod.inr ≫ s.inl))

Tactic:
simp [← h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan.{v₁, u₁} X Y
hc : IsColimit c
I : C
hI : IsInitial.{v₁, u₁} I
⊢ ∀
    (s :
      PushoutCocone (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
        (Z := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
        (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
        (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))),
    c.inr ≫
        (fun
              (s :
                PushoutCocone (Y :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                  (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
                  (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
            BinaryCofan.IsColimit.desc hc s.inr s.inl)
          s =
      s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan.{v₁, u₁} X Y
hc : IsColimit c
I : C
hI : IsInitial.{v₁, u₁} I
⊢ ∀
    (s :
      PushoutCocone (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
        (Z := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
        (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
        (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))),
    c.inl ≫
        (fun
              (s :
                PushoutCocone (Y :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                  (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
                  (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
            BinaryCofan.IsColimit.desc hc s.inr s.inl)
          s =
      s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan.{v₁, u₁} X Y
hc : IsColimit c
I : C
hI : IsInitial.{v₁, u₁} I
s :
  PushoutCocone (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
m :
  Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
h₃ :
  c.inl ≫ m =
    c.inl ≫
      (fun
            (s :
              PushoutCocone (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
          BinaryCofan.IsColimit.desc hc s.inr s.inl)
        s
h₄ :
  c.inr ≫ m =
    c.inr ≫
      (fun
            (s :
              PushoutCocone (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
          BinaryCofan.IsColimit.desc hc s.inr s.inl)
        s
⊢ m =
    (fun
          (s :
            PushoutCocone (Y :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
        BinaryCofan.IsColimit.desc hc s.inr s.inl)
      s

Tactic:
apply BinaryCofan.IsColimit.hom_ext hc

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- 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
w : f ≫ inl = g ≫ inr
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : P ⟶ T⦄, inl ≫ φ = inl ≫ φ' → inr ≫ φ = inr ≫ φ' → φ = φ'
exists_desc : ∀ ⦃T : C⦄ (a : X ⟶ T) (b : Y ⟶ T), f ≫ a = g ≫ b → ∃ (l : P ⟶ T), inl ≫ l = a ∧ inr ≫ l = b
l : ∀ (s : PushoutCocone f g), ∃ (l : P ⟶ s.pt), inl ≫ l = s.inl ∧ inr ≫ l = s.inr := ⋯
⊢ Nonempty (IsColimit (PushoutCocone.mk inl inr w))

Tactic:
⟨PushoutCocone.IsColimit.mk _
      (fun s ↦ (l s).choose)
      (fun s ↦ (l s).choose_spec.1)
      (fun s ↦ (l s).choose_spec.2)
      (fun s m h₁ h₂ ↦ hom_ext
        (h₁.trans (l s).choose_spec.1.symm)
        (h₂.trans (l s).choose_spec.2.symm))⟩

Premises used: Exists.choose_spec, CategoryTheory.Limits.PushoutCocone.IsColimit.mk, Nonempty.intro, And.right, And.left, Exists.choose, Eq.symm, Eq.trans
-- 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
w : f ≫ inl = g ≫ inr
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : P ⟶ T⦄, inl ≫ φ = inl ≫ φ' → inr ≫ φ = inr ≫ φ' → φ = φ'
exists_desc : ∀ ⦃T : C⦄ (a : X ⟶ T) (b : Y ⟶ T), f ≫ a = g ≫ b → ∃ (l : P ⟶ T), inl ≫ l = a ∧ inr ≫ l = b
l : ∀ (s : PushoutCocone f g), ∃ (l : P ⟶ s.pt), inl ≫ l = s.inl ∧ inr ≫ l = s.inr := ⋯
⊢ Nonempty (IsColimit (PushoutCocone.mk inl inr w))

Tactic:
exact ⟨PushoutCocone.IsColimit.mk _
      (fun s ↦ (l s).choose)
      (fun s ↦ (l s).choose_spec.1)
      (fun s ↦ (l s).choose_spec.2)
      (fun s m h₁ h₂ ↦ hom_ext
        (h₁.trans (l s).choose_spec.1.symm)
        (h₂.trans (l s).choose_spec.2.symm))⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
lift : (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt
fac : ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι
uniq :
  ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
fapply Fork.IsLimit.mk

Premises used: CategoryTheory.Limits.Fork.IsLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt

Tactic:
exact fun s => H.isLimit.lift (PullbackCone.mk s.ι s.ι s.condition)

Premises used: CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι

Tactic:
fun s => H.isLimit.fac _ WalkingCospan.left

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.Fork.condition, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.cospan, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι

Tactic:
exact fun s => H.isLimit.fac _ WalkingCospan.left

Premises used: CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
uniq₁ : m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext H.isLimit

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

Tactic:
e.trans ?_

Premises used: CategoryTheory.Limits.Fork.ι, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
⊢ m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

Tactic:
refine e.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd

Tactic:
e.trans ?_

Premises used: CategoryTheory.Limits.Fork.ι, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
⊢ m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd

Tactic:
refine e.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι

Tactic:
H.isLimit.fac _ _

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.cospan, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι

Tactic:
exact H.isLimit.fac _ _

Premises used: CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι

Tactic:
H.isLimit.fac _ _

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.cospan, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι

Tactic:
exact H.isLimit.fac _ _

Premises used: CategoryTheory.Limits.IsLimit.fac, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
desc : (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt
fac : ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
uniq :
  ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
⊢ IsColimit (Cofork.ofπ g ⋯)

Tactic:
fapply Cofork.IsColimit.mk

Premises used: CategoryTheory.Limits.Cofork.IsColimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt

Tactic:
exact fun s => H.isColimit.desc (PushoutCocone.mk s.π s.π s.condition)

Premises used: CategoryTheory.Limits.IsColimit.desc, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.PushoutCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
fun s => H.isColimit.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.Cofork.condition, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.PushoutCocone.mk, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
exact fun s => H.isColimit.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
uniq₁ : H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
e.trans ?_

Premises used: Eq.trans, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
⊢ H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
refine e.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
e.trans ?_

Premises used: Eq.trans, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
⊢ H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
refine e.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
⊢ s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
⊢ s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
H.isColimit.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
exact H.isColimit.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
H.isColimit.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
exact H.isColimit.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
      (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
        (isLimitOfPreserves F s.isLimit))

Premises used: CategoryTheory.Functor.map_commSq, CategoryTheory.Limits.cospanCompIso, CategoryTheory.IsPullback.toCommSq, CategoryTheory.IsPullback.of_isLimit', DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso, CategoryTheory.Limits.WalkingCospan.ext, CategoryTheory.IsPullback.isLimit