awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i j : ι
hij : i ≠ j
t : PullbackCone (d.inj i) (d.inj j)
ht : IsLimit t
e : d ≅ c := hd.uniqueUpToIso hc
heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
u : t.pt ⟶ (s hij).pt := PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ⋯
⊢ (u ≫ (H hij).to t.pt) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Tactic:
simp [show (H hij).to (X j) = (s hij).snd from (H hij).hom_ext _ _, u]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i : ι
⊢ d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i : ι
rw : Mono (c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom)
⊢ Mono (d.inj i)

Tactic:
rw [show d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom by simp]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
inst_1 : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
d : Cofan.{u_1, v, u} X
hd : IsColimit d
i : ι
⊢ Mono (c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : HasCoproduct.{u_1, v, u} X
inst_2 : ∀ (i : ι), Mono.{v, u} (Y := sigmaObj.{u_1, v, u} X) (Sigma.ι X i)
s : {i j : ι} → i ≠ j → PullbackCone.{v, u} (Z := sigmaObj.{u_1, v, u} X) (Sigma.ι X i) (Sigma.ι X j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial.{v, u} (s hij).pt
⊢ CoproductDisjoint.{v, u, u_1} X

Tactic:
have (i : ι) : Mono ((Cofan.mk (∐ X) (Sigma.ι X)).inj i) := inferInstanceAs <| Mono (Sigma.ι X i)
  .of_cofan (coproductIsCoproduct X) s hs H

Premises used: _private.0.CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct._proof_1, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.CoproductDisjoint.of_cofan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
i : ι
⊢ Mono (c.inj i)

Tactic:
CoproductDisjoint.mono_inj hc i

Premises used: CategoryTheory.Limits.CoproductDisjoint.mono_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
inst_2 : HasCoproduct.{u_1, v, u} X
i : ι
⊢ Mono.{v, u} (Y := sigmaObj.{u_1, v, u} X) (Sigma.ι X i)

Tactic:
CoproductDisjoint.mono_inj (colimit.isColimit _) i

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.CoproductDisjoint.mono_inj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ CommSq (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
refine_1 : Y ≅ pullback (c.inj i) (c.inj j)
refine_2 :
  CategoryStruct.comp (Y := pullback (c.inj i) (c.inj j))
      (Iso.hom (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)))
      (pullback.fst (c.inj i) (c.inj j)) =
    hY.to (X i)
refine_3 :
  CategoryStruct.comp (Y := pullback (c.inj i) (c.inj j))
      (Iso.hom (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)))
      (pullback.snd (c.inj i) (c.inj j)) =
    hY.to (X j)
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)

Tactic:
refine .of_iso_pullback (by simp) ?_ ?_ ?_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
refine_1 : IsInitial.{v, u} (pullback (c.inj i) (c.inj j))
⊢ Y ≅ pullback (c.inj i) (c.inj j)

Tactic:
refine hY.uniqueUpToIso ?_

Premises used: CategoryTheory.Limits.IsInitial.uniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ IsInitial.{v, u} (pullback (c.inj i) (c.inj j))

Tactic:
exact IsInitial.ofCoproductDisjointOfIsColimit hij hc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ CategoryStruct.comp (Y := pullback (c.inj i) (c.inj j))
      (Iso.hom (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)))
      (pullback.fst (c.inj i) (c.inj j)) =
    hY.to (X i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
inst_1 : CoproductDisjoint.{v, u, u_1} X
c : Cofan.{u_1, v, u} X
hc : IsColimit c
Y : C
hY : IsInitial.{v, u} Y
i j : ι
inst_2 : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ CategoryStruct.comp (Y := pullback (c.inj i) (c.inj j))
      (Iso.hom (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)))
      (pullback.snd (c.inj i) (c.inj j)) =
    hY.to (X j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
i : WalkingPair
left : Mono (Cofan.inj c WalkingPair.left)
right : Mono (Cofan.inj c WalkingPair.right)
⊢ Mono (Cofan.inj c i)

Tactic:
cases i
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
⊢ Mono (Cofan.inj c WalkingPair.left)

Tactic:
inferInstanceAs <| Mono c.inl

Premises used: _private.0.CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
⊢ Mono (Cofan.inj c WalkingPair.left)

Tactic:
exact inferInstanceAs <| Mono c.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
⊢ Mono (Cofan.inj c WalkingPair.right)

Tactic:
inferInstanceAs <| Mono c.inr

Premises used: _private.0.CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan._proof_2
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
⊢ Mono (Cofan.inj c WalkingPair.right)

Tactic:
exact inferInstanceAs <| Mono c.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
⊢ ∀ (i : WalkingPair), Mono (Cofan.inj c i)

Tactic:
have (i : WalkingPair) : Mono (Cofan.inj c i) := by
    cases i
    · exact inferInstanceAs <| Mono c.inl
    · exact inferInstanceAs <| Mono c.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
⊢ BinaryCoproductDisjoint.{v, u} X Y

Tactic:
.of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)

Premises used: CategoryTheory.Limits.CoproductDisjoint.of_cofan
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
refine_1 : {i j : WalkingPair} → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)
refine_2 :
  {i j : WalkingPair} →
    (hij : i ≠ j) →
      IsLimit.{0, v, 0, u} (J := WalkingCospan) (C := C) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
        ((fun {i j : WalkingPair} (hij : i ≠ j) ↦
            (match (motive := (i j : WalkingPair) → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
                hij with
              | WalkingPair.left, WalkingPair.right, hij => s
              | WalkingPair.right, WalkingPair.left, hij => s.flip :
              PullbackCone (Cofan.inj c i) (Cofan.inj c j)))
          hij)
refine_3 :
  {i j : WalkingPair} →
    (hij : i ≠ j) →
      IsInitial.{v, u} (C := C)
        (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
          ((fun {i j : WalkingPair} (hij : i ≠ j) ↦
              (match (motive := (i j : WalkingPair) → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i,
                  j, hij with
                | WalkingPair.left, WalkingPair.right, hij => s
                | WalkingPair.right, WalkingPair.left, hij => s.flip :
                PullbackCone (Cofan.inj c i) (Cofan.inj c j)))
            hij))
⊢ BinaryCoproductDisjoint.{v, u} X Y

Tactic:
refine .of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ PullbackCone (Cofan.inj c WalkingPair.left) (Cofan.inj c WalkingPair.right)

Tactic:
exact s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ PullbackCone (Cofan.inj c WalkingPair.right) (Cofan.inj c WalkingPair.left)

Tactic:
exact s.flip

Premises used: CategoryTheory.Limits.PullbackCone.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ PullbackCone (Cofan.inj c i) (Cofan.inj c j)

Tactic:
match i, j with
    | .left, .right => exact s
    | .right, .left => exact s.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
refine_2 :
  IsLimit.{0, v, 0, u} (J := WalkingCospan) (C := C) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
    (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
      hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip)
⊢ IsLimit.{0, v, 0, u} (J := WalkingCospan) (C := C) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
    ((fun {i j : WalkingPair} (hij : i ≠ j) ↦
        (match (motive := (i j : WalkingPair) → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
            hij with
          | WalkingPair.left, WalkingPair.right, hij => s
          | WalkingPair.right, WalkingPair.left, hij => s.flip :
          PullbackCone (Cofan.inj c i) (Cofan.inj c j)))
      hij)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsLimit s
h_2 : (i j : WalkingPair) → i ≠ j → WalkingPair.right ≠ WalkingPair.left → IsLimit s.flip
⊢ IsLimit.{0, v, 0, u} (J := WalkingCospan) (C := C) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
    (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
      hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip)

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
hij_1 : WalkingPair.left ≠ WalkingPair.right
⊢ IsLimit s

Tactic:
exact hs
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
hij_1 : WalkingPair.right ≠ WalkingPair.left
⊢ IsLimit s.flip

Tactic:
exact PullbackCone.flipIsLimit hs

Premises used: CategoryTheory.Limits.PullbackCone.flipIsLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
refine_3 :
  IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
        hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip))
⊢ IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      ((fun {i j : WalkingPair} (hij : i ≠ j) ↦
          (match (motive := (i j : WalkingPair) → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
              hij with
            | WalkingPair.left, WalkingPair.right, hij => s
            | WalkingPair.right, WalkingPair.left, hij => s.flip :
            PullbackCone (Cofan.inj c i) (Cofan.inj c j)))
        hij))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsInitial.{v, u} s.pt
h_2 : (i j : WalkingPair) → i ≠ j → WalkingPair.right ≠ WalkingPair.left → IsInitial.{v, u} s.flip.pt
⊢ IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
        hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip))

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
hij_1 : WalkingPair.left ≠ WalkingPair.right
⊢ IsInitial.{v, u} s.pt

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
hij_1 : WalkingPair.right ≠ WalkingPair.left
⊢ IsInitial.{v, u} s.flip.pt

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ Mono c.inl

Tactic:
.of_coproductDisjoint hc .left

Premises used: CategoryTheory.Mono.of_coproductDisjoint, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ Mono c.inr

Tactic:
.of_coproductDisjoint hc .right

Premises used: CategoryTheory.Mono.of_coproductDisjoint, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
Z : C
f : X ⟶ Z
g : Y ⟶ Z
hc : IsColimit (BinaryCofan.mk f g)
⊢ Mono f

Tactic:
.of_coproductDisjoint hc .left

Premises used: CategoryTheory.Mono.of_coproductDisjoint, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
Z : C
f : X ⟶ Z
g : Y ⟶ Z
hc : IsColimit (BinaryCofan.mk f g)
⊢ Mono g

Tactic:
.of_coproductDisjoint hc .right

Premises used: CategoryTheory.Mono.of_coproductDisjoint, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Mono.{v, u} (C := C) (X := X) (Y := coprod.{v, u} X Y) coprod.inl

Tactic:
@Mono.ι_of_coproductDisjoint _ _ _ _ _ ‹_› WalkingPair.left

Premises used: CategoryTheory.Mono.ι_of_coproductDisjoint, CategoryTheory.Limits.pair, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
inst_2 : HasBinaryCoproduct.{v, u} X Y
⊢ Mono.{v, u} (C := C) (X := Y) (Y := coprod.{v, u} X Y) coprod.inr

Tactic:
@Mono.ι_of_coproductDisjoint _ _ _ _ _ ‹_› WalkingPair.right

Premises used: CategoryTheory.Mono.ι_of_coproductDisjoint, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : BinaryCoproductDisjoint.{v, u} X Y
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
s : PullbackCone c.inl c.inr
hs : IsLimit s
⊢ WalkingPair.left ≠ WalkingPair.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
⊢ BinaryCoproductDisjoint.{v, u} (X WalkingPair.left) (X WalkingPair.right)

Tactic:
H (X .left) (X .right)

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
h :
  ∀ (x : WalkingPair),
    X x = WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x (X WalkingPair.left) (X WalkingPair.right)
⊢ CoproductDisjoint.{v, u, 0} X

Tactic:
convert! H (X .left) (X .right) using 2

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
x : WalkingPair
h :
  X WalkingPair.left =
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left (X WalkingPair.left)
      (X WalkingPair.right)
h₁ :
  X WalkingPair.right =
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right (X WalkingPair.left)
      (X WalkingPair.right)
⊢ X x = WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x (X WalkingPair.left) (X WalkingPair.right)

Tactic:
casesm WalkingPair

Premises used: CategoryTheory.Limits.WalkingPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
⊢ X WalkingPair.left =
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left (X WalkingPair.left)
      (X WalkingPair.right)

Tactic:
simp