awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
apply : ∀ (j : WidePullbackShape ι), k ≫ s.π.app j = l ≫ s.π.app j
⊢ k = l

Tactic:
apply hs.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ Eq (α := W ⟶ (WidePullbackShape.wideCospan X Y f).obj none) (k ≫ s.π.app none) (l ≫ s.π.app none)

Tactic:
hbase

Premises used: CategoryTheory.Limits.WidePullbackCone.base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ Eq (α := W ⟶ (WidePullbackShape.wideCospan X Y f).obj none) (k ≫ s.π.app none) (l ≫ s.π.app none)

Tactic:
exact hbase
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ Eq (α := W ⟶ (WidePullbackShape.wideCospan X Y f).obj (some j)) (k ≫ s.π.app (some j)) (l ≫ s.π.app (some j))

Tactic:
hπ j

Premises used: CategoryTheory.Limits.WidePullbackCone.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ Eq (α := W ⟶ (WidePullbackShape.wideCospan X Y f).obj (some j)) (k ≫ s.π.app (some j)) (l ≫ s.π.app (some j))

Tactic:
exact hπ j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
b : W ⟶ X
a : (i : ι) → W ⟶ Y i
w : ∀ (i : ι), a i ≫ f i = b
⊢ lift hs b a w ≫ s.base = b

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.WidePullbackCone.base, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
b : W ⟶ X
a : (i : ι) → W ⟶ Y i
w : ∀ (i : ι), a i ≫ f i = b
i : ι
⊢ lift hs b a w ≫ s.π i = a i

Tactic:
hs.fac _ _

Premises used: CategoryTheory.Limits.WidePullbackCone.π, CategoryTheory.Limits.WidePullbackCone.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ Eq (α :=
    Functor.obj.{u_2, v, u_2, u} (C := WidePullbackShape ι) (Functor.obj (Functor.const (WidePullbackShape ι)) s.pt)
        none ⟶
      (WidePullbackShape.wideCospan X Y f).obj none)
    (s.π.app none) (e.hom ≫ t.π.app none)

Tactic:
base.symm

Premises used: CategoryTheory.Limits.WidePullbackCone.base, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ Eq (α :=
    Functor.obj.{u_2, v, u_2, u} (C := WidePullbackShape ι) (Functor.obj (Functor.const (WidePullbackShape ι)) s.pt)
        none ⟶
      (WidePullbackShape.wideCospan X Y f).obj none)
    (s.π.app none) (e.hom ≫ t.π.app none)

Tactic:
exact base.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val : ι
⊢ Eq (α :=
    Functor.obj.{u_2, v, u_2, u} (Functor.obj (Functor.const (WidePullbackShape ι)) s.pt) (some val) ⟶
      (WidePullbackShape.wideCospan X Y f).obj (some val))
    (s.π.app (some val)) (e.hom ≫ t.π.app (some val))

Tactic:
(π _).symm

Premises used: CategoryTheory.Limits.WidePullbackCone.π, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val : ι
⊢ Eq (α :=
    Functor.obj.{u_2, v, u_2, u} (Functor.obj (Functor.const (WidePullbackShape ι)) s.pt) (some val) ⟶
      (WidePullbackShape.wideCospan X Y f).obj (some val))
    (s.π.app (some val)) (e.hom ≫ t.π.app (some val))

Tactic:
exact (π _).symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ ∀ (i : ι'),
    CategoryStruct.comp (Y := Y ((e : (a : ι') → ι) i))
        ((fun (i : ι') ↦ (s.π ((e : (a : ι') → ι) i) : s.pt ⟶ Y ((e : (a : ι') → ι) i))) i) (f ((e : (a : ι') → ι) i)) =
      s.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ (s.reindex e).base = s.base

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackCone.reindex, CategoryTheory.Limits.WidePullbackCone.mk, CategoryTheory.Limits.WidePullbackShape.mkCone, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.WidePullbackCone.base, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι'
⊢ (s.reindex e).π i = s.π ((e : (a : ι') → ι) i)

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePullbackCone.π, CategoryTheory.Limits.WidePullbackShape, CategoryTheory.Limits.WidePullbackCone.reindex, CategoryTheory.Limits.WidePullbackCone.mk, CategoryTheory.Limits.WidePullbackShape.mkCone, CategoryTheory.Limits.WidePullbackShape.wideCospan, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ Functor.obj.{u_2, v, u_2, u}
      ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
        WidePullbackShape.wideCospan X (fun (i : ι') ↦ Y ((e : (a : ι') → ι) i)) fun (i : ι') ↦
          f ((e : (a : ι') → ι) i))
      (some i) =
    (WidePullbackShape.wideCospan X Y f).obj (some i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ Eq (α :=
    Functor.obj.{u_2, v, u_2, u}
        ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
          WidePullbackShape.wideCospan X (fun (i : ι') ↦ Y ((e : (a : ι') → ι) i)) fun (i : ι') ↦
            f ((e : (a : ι') → ι) i))
        (some i) ⟶
      (WidePullbackShape.wideCospan X Y f).obj none)
    (Functor.map
        ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
          WidePullbackShape.wideCospan X (fun (i : ι') ↦ Y ((e : (a : ι') → ι) i)) fun (i : ι') ↦
            f ((e : (a : ι') → ι) i))
        (WidePullbackShape.Hom.term i) ≫
      Iso.hom (Iso.refl X))
    (Iso.hom
        ((fun (i : ι) ↦
            (eqToIso ⋯ :
              Functor.obj.{u_2, v, u_2, u}
                  ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
                    WidePullbackShape.wideCospan X (fun (i : ι') ↦ Y ((e : (a : ι') → ι) i)) fun (i : ι') ↦
                      f ((e : (a : ι') → ι) i))
                  (some i) ≅
                (WidePullbackShape.wideCospan X Y f).obj (some i)))
          i) ≫
      (WidePullbackShape.wideCospan X Y f).map (WidePullbackShape.Hom.term i))

Tactic:
simp [← eqToHom_naturality]

Premises used: CategoryTheory.eqToHom_naturality
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F := WidePullbackShape.wideCospan X Y f)
            (Functor.obj
              (Cone.postcompose (Iso.hom (WidePullbackShape.functorExt (Iso.refl X) (fun (i : ι) ↦ eqToIso ⋯) ⋯)))
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))))) ≫
      s.base =
    base
      (Functor.obj (Cone.postcompose (Iso.hom (WidePullbackShape.functorExt (Iso.refl X) (fun (i : ι) ↦ eqToIso ⋯) ⋯)))
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))

Tactic:
simp [base, reindex, mk]

Premises used: CategoryTheory.Limits.WidePullbackCone.reindex, CategoryTheory.Limits.WidePullbackCone.mk, CategoryTheory.Limits.WidePullbackCone.base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι_1 : Type u_1
X_1 : C
Y_1 : ι_1 → C
f_1 : (i : ι_1) → Y_1 i ⟶ X_1
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F := WidePullbackShape.wideCospan X Y f)
            (Functor.obj
              (Cone.postcompose (Iso.hom (WidePullbackShape.functorExt (Iso.refl X) (fun (i : ι) ↦ eqToIso ⋯) ⋯)))
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))))) ≫
      s.π i =
    π
      (Functor.obj (Cone.postcompose (Iso.hom (WidePullbackShape.functorExt (Iso.refl X) (fun (i : ι) ↦ eqToIso ⋯) ⋯)))
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))
      i

Tactic:
simp [π, reindex, mk,
            eqToHom_naturality (fun i ↦ (Cone.π s).app (some i)) (e.apply_symm_apply i)]

Premises used: CategoryTheory.Limits.Cone.π, Equiv.apply_symm_apply, CategoryTheory.Limits.WidePullbackCone.π, CategoryTheory.Limits.WidePullbackCone.reindex, Option.some, CategoryTheory.Limits.WidePullbackCone.mk, CategoryTheory.eqToHom_naturality, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
j : J
⊢ Eq (α := B ⟶ widePushout B objs arrows) (arrows j ≫ ι arrows j) (head arrows)

Tactic:
apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
j : J
⊢ CategoryStruct.comp (Y := widePushout B objs arrows) (ι arrows j) (desc f fs w) = fs j

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Premises used: CategoryTheory.Limits.WidePushoutShape.mkCocone_pt, CategoryTheory.Limits.WidePushoutShape.mkCocone_ι_app, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
⊢ CategoryStruct.comp (Y := widePushout B objs arrows) (head arrows) (desc f fs w) = f

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_pt, WidePushoutShape.mkCocone_ι_app]

Premises used: CategoryTheory.Limits.WidePushoutShape.mkCocone_pt, CategoryTheory.Limits.WidePushoutShape.mkCocone_ι_app, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
x :
  ∀ (j : WidePushoutShape J),
    (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app j ≫ g =
      NatTrans.app (Cocone.ι (WidePushoutShape.mkCocone f fs w)) j
⊢ g = desc f fs w

Tactic:
apply
    (colimit.isColimit (WidePushoutShape.wideSpan B objs arrows)).uniq
      (WidePushoutShape.mkCocone f fs <| w)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.WidePushoutShape.mkCocone
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ Eq (α :=
    (WidePushoutShape.wideSpan B objs arrows).obj none ⟶
      Cocone.pt.{w, v, w, u} (J := WidePushoutShape J) (F := WidePushoutShape.wideSpan B objs arrows)
        (WidePushoutShape.mkCocone f fs w))
    ((colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g)
    (NatTrans.app (Cocone.ι (WidePushoutShape.mkCocone f fs w)) none)

Tactic:
apply h2
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val : J
⊢ Eq (α :=
    (WidePushoutShape.wideSpan B objs arrows).obj (some val) ⟶
      Cocone.pt.{w, v, w, u} (J := WidePushoutShape J) (F := WidePushoutShape.wideSpan B objs arrows)
        (WidePushoutShape.mkCocone f fs w))
    ((colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val) ≫ g)
    (NatTrans.app (Cocone.ι (WidePushoutShape.mkCocone f fs w)) (some val))

Tactic:
apply h1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_2 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
rw : (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
⊢ arrows j ≫ (fun (j : J) ↦ ι arrows j ≫ g) j = head arrows ≫ g

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_2 : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
w :
  ∀ (j : WidePushoutShape J),
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g1 =
      colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g2
⊢ g1 = g2

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ Eq (α := (WidePushoutShape.wideSpan B objs arrows).obj none ⟶ X)
    (colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1)
    (colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2)

Tactic:
apply h2
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst_1 : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val : J
⊢ Eq (α := (WidePushoutShape.wideSpan B objs arrows).obj (some val) ⟶ X)
    (colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val) ≫ g1)
    (colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val) ≫ g2)

Tactic:
apply h1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWidePushouts C
⊢ HasWidePushouts.{w, v, u} C

Tactic:
fun _ =>
  hasColimitsOfShape_of_equivalence (WidePushoutShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

Premises used: Equiv.ulift, CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasWidePullbacks C
⊢ HasWidePullbacks.{w, v, u} C

Tactic:
fun _ =>
  hasLimitsOfShape_of_equivalence (WidePullbackShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

Premises used: Equiv.ulift, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := X ⟶ Z) (f ≫ 0) 0

Tactic:
HasZeroMorphisms.comp_zero f Z

Premises used: CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) (0 ≫ f) 0

Tactic:
HasZeroMorphisms.zero_comp X f

Premises used: CategoryTheory.Limits.HasZeroMorphisms.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : X ⟶ Y
⊢ Zero (X ⟶ Y)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : PLift (X.as = Y.as)
⊢ X ⟶ Y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : X.as = Y.as
⊢ PLift (X.as = Y.as)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
⊢ X.as = Y.as

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : Discrete PUnit.{u_1 + 1}
zero : X ⟶ Y
zero₁ : PLift (X.as = Y.as)
zero₂ : X.as = Y.as
⊢ Zero (X ⟶ Y)

Tactic:
repeat (constructor)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
h : ∀ (X Y : C), Eq.{v + 1} (α := Zero (X ⟶ Y)) (zero X Y) (zero X Y)
⊢ Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero

Tactic:
funext X Y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero

Tactic:
specialize w X Y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
w : Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
⊢ Eq.{v + 1} (α := Zero (X ⟶ Y)) (zero X Y) (zero X Y)

Tactic:
apply congrArg Zero.mk w

Premises used: congrArg, Zero.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
⊢ Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero

Tactic:
have : I.zero = J.zero := by
    funext X Y
    specialize w X Y
    apply congrArg Zero.mk w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) zero zero
mk :
  ∀ [zero : (X Y : C) → Zero (X ⟶ Y)] (comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0)
    (zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0)
    (w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero)
    (this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero),
    { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } = J
⊢ I = J

Tactic:
cases I
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
J : HasZeroMorphisms.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
mk :
  ∀ [zero_1 : (X Y : C) → Zero (X ⟶ Y)] (comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0)
    (zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0)
    (w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero)
    (this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero),
    { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } =
      { zero := zero_1, comp_zero := @comp_zero_1, zero_comp := zero_comp_1 }
⊢ { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } = J

Tactic:
cases J