awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
val : F.obj X
⊢ Eq (α := F.obj Z ⊕ G.obj Z)
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
            (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z))))
      (Sum.inl val))
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
              (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
                (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
              (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z)))))
      (Sum.inl val))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
val : G.obj X
⊢ Eq (α := F.obj Z ⊕ G.obj Z)
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
            (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
              (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z))))
      (Sum.inr val))
    (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
              (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
                (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
              (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
                (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z)))))
      (Sum.inr val))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x x_1 : C
x_2 : x ⟶ x_1
h :
  ∀ (val : F₁.obj x),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          ((coprod F₁ F₂).map x_2 ≫
            ↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
        (Sum.inl val) =
      TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
            F.map x_2))
        (Sum.inl val)
h₁ :
  ∀ (val : F₂.obj x),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          ((coprod F₁ F₂).map x_2 ≫
            ↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
        (Sum.inr val) =
      TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
        (hom (FC := TypeCat.Fun)
          (↾Sum.elim
                (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
                (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                  (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
            F.map x_2))
        (Sum.inr val)
⊢ (coprod F₁ F₂).map x_2 ≫
      ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1)) =
    ↾Sum.elim
          (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
          (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
            (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
      F.map x_2

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x x_1 : C
x_2 : x ⟶ x_1
val : F₁.obj x
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coprod F₁ F₂).map x_2 ≫
          ↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
      (Sum.inl val) =
    TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
          F.map x_2))
      (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x x_1 : C
x_2 : x ⟶ x_1
val : F₂.obj x
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((coprod F₁ F₂).map x_2 ≫
          ↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x_1)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))))
      (Sum.inr val) =
    TypeCat.Fun.toFun (X := (coprod F₁ F₂).obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.elim
              (⇑(hom (FC := TypeCat.Fun) (τ₁.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₁.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
              (⇑(hom (FC := TypeCat.Fun) (τ₂.app x)) :
                (a : (fun (X : Type w) ↦ X) (F₂.obj x)) → (fun (X : Type w) ↦ X) (F.obj x)) ≫
          F.map x_2))
      (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
⊢ inl ≫ desc τ₁ τ₂ = τ₁

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
⊢ inr ≫ desc τ₁ τ₂ = τ₂

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cocone (pair F G)
x_1 : (binaryCoproductCocone F G).pt ⟶ x.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_1 = x.ι.app j
w :
  ∀ (x_2 : C) (x_3 : (binaryCoproductCocone F G).pt.obj x_2),
    (hom (FC := TypeCat.Fun) (x_1.app x_2)).toFun x_3 =
      (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)).app x_2)).toFun x_3
⊢ x_1 = coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)

Tactic:
ext _ x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cocone (pair F G)
x_1 : (binaryCoproductCocone F G).pt ⟶ x.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_1 = x.ι.app j
x_2 : C
val : F.obj x_2
⊢ (hom (FC := TypeCat.Fun) (x_1.app x_2)).toFun (Sum.inl val) =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)).app x_2)).toFun (Sum.inl val)

Tactic:
simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cocone (pair F G)
x_1 : (binaryCoproductCocone F G).pt ⟶ x.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_1 = x.ι.app j
x_2 : C
val : G.obj x_2
⊢ (hom (FC := TypeCat.Fun) (x_1.app x_2)).toFun (Sum.inr val) =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x) (BinaryCofan.inr x)).app x_2)).toFun (Sum.inr val)

Tactic:
simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x_1 : Cocone (pair F G)
x_2 : (binaryCoproductCocone F G).pt ⟶ x_1.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x_2 = x_1.ι.app j
x_3 : C
x : (binaryCoproductCocone F G).pt.obj x_3
w :
  ∀ (val : F.obj x_3),
    (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun (Sum.inl val) =
      (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun (Sum.inl val)
w₁ :
  ∀ (val : G.obj x_3),
    (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun (Sum.inr val) =
      (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun (Sum.inr val)
⊢ (hom (FC := TypeCat.Fun) (x_2.app x_3)).toFun x =
    (hom (FC := TypeCat.Fun) ((coprod.desc (BinaryCofan.inl x_1) (BinaryCofan.inr x_1)).app x_3)).toFun x

Tactic:
cases x with | _ => simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ CategoryStruct.comp (Y := F ⨿ G) Limits.coprod.inl
      (Iso.hom (colimit.isoColimitCocone (binaryCoproductColimitCocone F G))) =
    coprod.inl

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : F.obj a
⊢ Eq (α := F.obj a ⊕ G.obj a)
    ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).hom.app a) : (a_1 : (F ⨿ G).obj a) → F.obj a ⊕ G.obj a)
        ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.coprod.inl a) : (a_1 : F.obj a) → (F ⨿ G).obj a) x :
          (F ⨿ G).obj a) :
      F.obj a ⊕ G.obj a)
    (Sum.inl x : F.obj a ⊕ G.obj a)

Tactic:
congr_hom (congr_app (inl_comp_binaryCoproductIso_hom F G) a) x

Premises used: CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
simp :
  Eq (α := G ⟶ coprod F G)
    ((binaryCoproductColimitCocone F G).cocone.ι.app { as := WalkingPair.right } :
      Functor.obj (pair F G) { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (binaryCoproductColimitCocone F G).cocone.pt)
          { as := WalkingPair.right : Discrete WalkingPair })
    coprod.inr
⊢ Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr

Tactic:
simp [binaryCoproductIso]

Premises used: CategoryTheory.FunctorToTypes.binaryCoproductIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ Eq (α := G ⟶ coprod F G)
    ((binaryCoproductColimitCocone F G).cocone.ι.app { as := WalkingPair.right } :
      Functor.obj (pair F G) { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (binaryCoproductColimitCocone F G).cocone.pt)
          { as := WalkingPair.right : Discrete WalkingPair })
    coprod.inr

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : G.obj a
⊢ Eq (α := F.obj a ⊕ G.obj a)
    ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).hom.app a) : (a_1 : (F ⨿ G).obj a) → F.obj a ⊕ G.obj a)
        ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.coprod.inr a) : (a_1 : G.obj a) → (F ⨿ G).obj a) x :
          (F ⨿ G).obj a) :
      F.obj a ⊕ G.obj a)
    (Sum.inr x : F.obj a ⊕ G.obj a)

Tactic:
congr_hom (congr_app (inr_comp_binaryCoproductIso_hom F G) a) x

Premises used: CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ coprod.inl ≫ (binaryCoproductIso F G).inv = Limits.coprod.inl

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.colimit, rfl, Sum.elim, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : F.obj a
⊢ Eq (α := (F ⨿ G).obj a)
    ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).inv.app a) : (a_1 : F.obj a ⊕ G.obj a) → (F ⨿ G).obj a)
        (Sum.inl x) :
      (F ⨿ G).obj a)
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.coprod.inl a) : (a_1 : F.obj a) → (F ⨿ G).obj a) x : (F ⨿ G).obj a)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
⊢ coprod.inr ≫ (binaryCoproductIso F G).inv = Limits.coprod.inr

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Limits.colimit, rfl, Sum.elim, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : G.obj a
⊢ Eq (α := (F ⨿ G).obj a)
    ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).inv.app a) : (a_1 : F.obj a ⊕ G.obj a) → (F ⨿ G).obj a)
        (Sum.inr x) :
      (F ⨿ G).obj a)
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.coprod.inr a) : (a_1 : G.obj a) → (F ⨿ G).obj a) x : (F ⨿ G).obj a)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : (F ⨿ G).obj a
⊢ (fun (z : F.obj a ⊕ G.obj a) ↦
        ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).inv.app a) :
              (a_1 : (fun (X : Type w) ↦ X) ((coprod F G).obj a)) → (fun (X : Type w) ↦ X) ((F ⨿ G).obj a))
            z :
          (fun (X : Type w) ↦ X) ((F ⨿ G).obj a)))
      ((fun (z : (F ⨿ G).obj a) ↦
          ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).hom.app a) :
                (a_1 : (fun (X : Type w) ↦ X) ((F ⨿ G).obj a)) → (fun (X : Type w) ↦ X) ((coprod F G).obj a))
              z :
            (fun (X : Type w) ↦ X) ((coprod F G).obj a)))
        x) =
    x

Tactic:
simp [-coprod_obj]

Premises used: CategoryTheory.FunctorToTypes.coprod_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
x : F.obj a ⊕ G.obj a
⊢ (fun (z : (F ⨿ G).obj a) ↦
        ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).hom.app a) :
              (a_1 : (fun (X : Type w) ↦ X) ((F ⨿ G).obj a)) → (fun (X : Type w) ↦ X) ((coprod F G).obj a))
            z :
          (fun (X : Type w) ↦ X) ((coprod F G).obj a)))
      ((fun (z : F.obj a ⊕ G.obj a) ↦
          ((hom (FC := TypeCat.Fun) ((binaryCoproductIso F G).inv.app a) :
                (a_1 : (fun (X : Type w) ↦ X) ((coprod F G).obj a)) → (fun (X : Type w) ↦ X) ((F ⨿ G).obj a))
              z :
            (fun (X : Type w) ↦ X) ((F ⨿ G).obj a)))
        x) =
    x

Tactic:
simp [-coprod_obj]

Premises used: CategoryTheory.FunctorToTypes.coprod_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
⊢ ∀ (X : C), HasColimit (Grothendieck.ι F X ⋙ G)

Tactic:
fun X => hasColimit_of_iso (F := (F.map (𝟙 _)).toFunctor ⋙ Grothendieck.ι F X ⋙ G) <|
    (leftUnitor (Grothendieck.ι F X ⋙ G)).symm ≪≫
    (isoWhiskerRight (eqToIso congr($((F.map_id X).symm).toFunctor)) (Grothendieck.ι F X ⋙ G))

Premises used: CategoryTheory.Grothendieck.ι, congrArg, CategoryTheory.eqToIso, CategoryTheory.Functor.comp, CategoryTheory.Limits.hasColimit_of_iso, id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, Eq.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
w :
  ∀ (d : (↑(F.obj X) : Type u_1)),
    CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
        (CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
          (colimMap
            (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
              ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
          (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor)) =
      colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))
⊢ CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
      (colimMap
        (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
          ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
      (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor) =
    𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (colimit.ι (Grothendieck.ι F X ⋙ G) d)
⊢ CategoryStruct.comp (Y := colimit (Grothendieck.ι F X ⋙ G)) (colimit.ι (Grothendieck.ι F X ⋙ G) d)
      (CategoryStruct.comp (Y := colimit ((F.map (𝟙 X)).toFunctor ⋙ Grothendieck.ι F X ⋙ G))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
            ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom))
        (colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor)) =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Grothendieck.ιNatTrans, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Grothendieck.ι_obj, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : (↑(F.obj X) : Type u_1)
⊢ (F.map (𝟙 X)).toFunctor.obj d = d

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : (↑(F.obj X) : Type u_1)
rw :
  CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d)) (eqToHom ⋯)
    (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d))
| colimit.ι (Grothendieck.ι F X ⋙ G) d

Tactic:
rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]

Premises used: CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.eqToHom_comp_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F X ⋙ G).obj ((F.map (𝟙 X)).toFunctor.obj d)) (eqToHom ⋯)
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
⊢ Eq (α := G.obj { base := X, fiber := d : Grothendieck F } ⟶ colimit (Grothendieck.ι F X ⋙ G))
    (CategoryStruct.comp (Y := G.obj { base := X, fiber := (F.map (𝟙 X)).toFunctor.obj d })
      (G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) })
      (colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)))
    (colimit.ι (Grothendieck.ι F X ⋙ G) d)

Tactic:
conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)]

Premises used: CategoryTheory.Grothendieck.ι, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.eqToHom_comp_ι