awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m ≫ snd (fst f g) (fst f h) =
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h))
have refine_4 : (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
  CategoryStruct.comp (Y := pullback f h)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry) (snd (fst f g) (fst f h)))
    (fst f h)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
refine_4 :
  (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    CategoryStruct.comp (Y := pullback f h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h)))
      (fst f h)
⊢ m ≫ snd (fst f g) (fst f h) =
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h))
have refine_4₁ : (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
  CategoryStruct.comp (Y := pullback f h)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry) (snd (fst f g) (fst f h)))
    (snd f h)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ Eq (α := Opposite.op Y ⟶ Opposite.op (codiagonalObj f))
    (Quiver.Hom.op (codiagonal f) : Opposite.op Y ⟶ Opposite.op (codiagonalObj f))
    (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
        (pullback.diagonal f.op) (Iso.hom (pullbackIsoOpPushout f.op f.op)) :
      Opposite.op Y ⟶ Opposite.op (pushout f.op.unop f.op.unop))
have rw : Eq (α := Opposite.op Y ⟶ pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
  (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.diagonal f.op)
Tactic: rw [← Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ Eq (α := Opposite.op Y ⟶ pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.diagonal f.op)
have h₀ : CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.fst f.op f.op) =
  CategoryStruct.comp (Y :=
    pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
    (pullback.diagonal f.op) (pullback.fst f.op f.op)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
h₀ :
  CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.fst f.op f.op) =
    CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.diagonal f.op) (pullback.fst f.op f.op)
⊢ Eq (α := Opposite.op Y ⟶ pullback.diagonalObj.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op X) f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.diagonal f.op)
have h₁ : CategoryStruct.comp (Y := pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
    (Quiver.Hom.op (codiagonal f) ≫ Iso.inv (pullbackIsoOpPushout f.op f.op)) (pullback.snd f.op f.op) =
  CategoryStruct.comp (Y :=
    pullback.{v_1, u_1} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
    (pullback.diagonal f.op) (pullback.snd f.op f.op)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X_1 Y_1 Z X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
inst_2 : Epi f
⊢ IsIso (X := codiagonalObj f) (codiagonal f)
have rw : IsIso (X := codiagonalObj f) (inv (inl f f))
Tactic: rw [(IsIso.inv_eq_of_hom_inv_id (inl_codiagonal f)).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
H : IsIso (X := codiagonalObj f) (codiagonal f)
Z : C
x x_1 : Y ⟶ Z
e : f ≫ x = f ≫ x_1
⊢ x = x_1
have rw : CategoryStruct.comp (Y := pushout f f) (inl f f) (desc x x_1 e) = x_1
Tactic: rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
H : IsIso (X := codiagonalObj f) (codiagonal f)
Z : C
x x_1 : Y ⟶ Z
e : f ≫ x = f ≫ x_1
rw : CategoryStruct.comp (Y := pushout f f) (inl f f) (desc x x_1 e) = x_1
⊢ x = x_1
have rw₁ : CategoryStruct.comp (Y := pushout f f) (inr f f) (desc x x_1 e) = x_1
Tactic: rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
H : IsIso (X := codiagonalObj f) (codiagonal f)
Z : C
x x_1 : Y ⟶ Z
e : f ≫ x = f ≫ x_1
rw : CategoryStruct.comp (Y := pushout f f) (inl f f) (desc x x_1 e) = x_1
rw₁ : CategoryStruct.comp (Y := pushout f f) (inr f f) (desc x x_1 e) = x_1
⊢ x = x_1
have rw₂ : x_1 = x_1
Tactic: rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPushout (Z := pushout i i) (X := pushout (i ≫ f) (i ≫ g)) (P := pushout f g)
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯) (pushout.codiagonal i)
    (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯) (f ≫ pushout.inl f g)
have rw : IsPullback.{v_1, u_1} (C := Cᵒᵖ) (P := Opposite.op (pushout f g)) (X := Opposite.op T) (Y :=
  Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z := Opposite.op (pushout i i)) (Quiver.Hom.op (f ≫ pushout.inl f g))
  (Quiver.Hom.op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i sorry sorry)) (Quiver.Hom.op (pushout.codiagonal i))
  (Quiver.Hom.op (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) sorry sorry))
Tactic: rw [← IsPullback.op_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPushouts.{v_1, u_1} C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPullback.{v_1, u_1} (C := Cᵒᵖ) (P := Opposite.op (pushout f g)) (X := Opposite.op T) (Y :=
    Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z := Opposite.op (pushout i i)) (Quiver.Hom.op (f ≫ pushout.inl f g))
    (Quiver.Hom.op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯)) (Quiver.Hom.op (pushout.codiagonal i))
    (Quiver.Hom.op (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯))
have simp : IsPullback (P := Opposite.op (pushout f g)) (Y := Opposite.op (pushout (i ≫ f) (i ≫ g))) (Z :=
  Opposite.op (pushout i i)) (Quiver.Hom.op (pushout.inl f g) ≫ f.op : Opposite.op (pushout f g) ⟶ Opposite.op T)
  (CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op T) f.op g.op)
      (Iso.inv (pullbackIsoOpPushout f.op g.op))
      (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op))
        (pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op sorry sorry)
        (Iso.hom (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))) :
    Opposite.op (pushout f g) ⟶ Opposite.op (pushout (i ≫ f) (i ≫ g)))
  (CategoryStruct.comp (Y := pullback.diagonalObj.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op S) i.op)
      (pullback.diagonal i.op) (Iso.hom (pullbackIsoOpPushout i.op i.op)) :
    Opposite.op T ⟶ Opposite.op (pushout i i))
  (CategoryStruct.comp (Y :=
      pullback.{v_1, u_1} (X := Opposite.op X) (Y := Opposite.op Y) (Z := Opposite.op S) (f.op ≫ i.op) (g.op ≫ i.op))
      (Iso.inv (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)))
      (CategoryStruct.comp (Y :=
        pullback.{v_1, u_1} (X := Opposite.op T) (Y := Opposite.op T) (Z := Opposite.op S) i.op i.op)
        (pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) sorry sorry)
        (Iso.hom (pullbackIsoOpPushout i.op i.op))) :
    Opposite.op (pushout (i ≫ f) (i ≫ g)) ⟶ Opposite.op (pushout i i))
Tactic: simp only [op_pushoutMap, Quiver.Hom.unop_op, op_comp, unop_comp, op_id, pushout.op_codiagonal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (hypothesis)
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
⊢ Nonempty (IsInitial.{v, u} t.pt)
have heq : ∀ (i : ι), d.inj i ≫ e.hom.hom = c.inj i
Tactic: have heq (i) : d.inj i ≫ e.hom.hom = c.inj i := e.hom.w ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
⊢ t.pt ⟶ (s hij).pt
have refine : t.fst ≫ c.inj i = t.snd ≫ c.inj j
Tactic: refine PullbackCone.IsLimit.lift (hs hij) t.fst t.snd ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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 ⋯
⊢ Nonempty (IsInitial.{v, u} t.pt)
have refine : u ≫ (H hij).to t.pt = 𝟙 t.pt
Tactic: refine ⟨(H hij).ofIso ⟨(H hij).to t.pt, u, (H hij).hom_ext _ _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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.pt
have refine_1 : (u ≫ (H hij).to t.pt) ≫ t.fst = 𝟙 t.pt ≫ t.fst
Tactic: refine PullbackCone.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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 ⋯
refine_1 : (u ≫ (H hij).to t.pt) ≫ t.fst = 𝟙 t.pt ≫ t.fst
⊢ u ≫ (H hij).to t.pt = 𝟙 t.pt
have refine_2 : (u ≫ (H hij).to t.pt) ≫ t.snd = 𝟙 t.pt ≫ t.snd
Tactic: refine PullbackCone.IsLimit.hom_ext ht ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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 (d.inj i)
have rw : Mono (c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom)
Tactic: rw [show d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom by simp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
have refine_1 : Y ≅ pullback (c.inj i) (c.inj j)
Tactic: refine .of_iso_pullback (by simp) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
have 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)
Tactic: refine .of_iso_pullback (by simp) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
⊢ IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
have 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)
Tactic: refine .of_iso_pullback (by simp) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
⊢ Y ≅ pullback (c.inj i) (c.inj j)
have refine_1 : IsInitial.{v, u} (pullback (c.inj i) (c.inj j))
Tactic: refine hY.uniqueUpToIso ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
have left : Mono (Cofan.inj c WalkingPair.left)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
⊢ Mono (Cofan.inj c i)
have right : Mono (Cofan.inj c WalkingPair.right)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (hypothesis)
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
⊢ BinaryCoproductDisjoint.{v, u} X Y
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
have refine_1 : {i j : WalkingPair} → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)
Tactic: refine .of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
⊢ BinaryCoproductDisjoint.{v, u} X Y
have 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)
Tactic: refine .of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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)
⊢ BinaryCoproductDisjoint.{v, u} X Y
have 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))
Tactic: refine .of_cofan hc (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_) (fun {i j} hij ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
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
⊢ 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)
have h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsLimit s
Tactic: split
Cleared hypotheses: i, j, hij