awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
⊢ ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r

Tactic:
fun j => ⟨_, isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j⟩

Premises used: CategoryTheory.GradedObject.cofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
inst_7 : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
dsimp :
  Eq (α :=
    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
      (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.inv (CofanMapObjFun.iso (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j))))
    (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
⊢ Eq (α :=
    (((bifunctorComp₂₃ F G₂₃).obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
      (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.hom (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃) j))
    (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
dsimp [mapBifunctorComp₂₃MapObjIso]

Premises used: CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
inst_7 : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ Eq (α :=
    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
      (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.inv (CofanMapObjFun.iso (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j))))
    (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
apply CofanMapObjFun.ιMapObj_iso_inv

Premises used: CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
inst_7 : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ Eq (α :=
    (F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
      (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.inv (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃) j))
    (ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
CofanMapObjFun.inj_iso_hom
    (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) _ h

Premises used: CategoryTheory.GradedObject.mapBifunctorMapObj, CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom, setOf, CategoryTheory.Discrete.functor, CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.Cofan.inj, Set.preimage, CategoryTheory.GradedObject.mapObj, CategoryTheory.GradedObject.mapTrifunctorMapObj, CategoryTheory.GradedObject.ιMapTrifunctorMapObj
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
h₁ :
  ∀ (i : (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9))),
    Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ f =
      Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ g
⊢ f = g

Tactic:
apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)

Premises used: CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i : I₁ × I₂ × I₃
hi : i ∈ r ⁻¹' {j}
⊢ Eq (α :=
    ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).mapObjFun r j
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ⟶
      A)
    (Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ≫
      f)
    (Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ≫
      g)

Tactic:
h _ _ _ hi

Premises used: CategoryTheory.GradedObject.mapBifunctorMapObj, setOf, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.Cofan.inj, Set.preimage, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i : I₁ × I₂ × I₃
hi : i ∈ r ⁻¹' {j}
⊢ Eq (α :=
    ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).mapObjFun r j
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ⟶
      A)
    (Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ≫
      f)
    (Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
        (Subtype.mk (p := fun (x : I₁ × I₂ × I₃) ↦ x ∈ r ⁻¹' {j}) i hi) ≫
      g)

Tactic:
exact h _ _ _ hi
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_6 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
A : C₄
f : (i₁ : I₁) → (i₂ : I₂) → (i₃ : I₃) → r (i₁, i₂, i₃) = j → ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶ A)
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : r (i₁, i₂, i₃) = j
⊢ CategoryStruct.comp (Y := mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
      (ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (mapBifunctorBifunctor₂₃Desc f) =
    f i₁ i₂ i₃ h

Tactic:
Cofan.IsColimit.fac
    (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) _ ⟨_, h⟩

Premises used: CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc, CategoryTheory.GradedObject.mapBifunctorMapObj, setOf, CategoryTheory.Discrete.functor, CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.colimit, Subtype.mk, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj, CategoryTheory.Limits.Cofan.inj, Set.preimage, CategoryTheory.GradedObject.mapObj, CategoryTheory.Limits.Cofan.IsColimit.fac
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h h₁ : ∀ (x : β), f x = g x
⊢ f = g

Tactic:
funext
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
x : β
⊢ f x = g x

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
change : IsIso (Iso.hom (X.isoMk Y fun (i : β) ↦ asIso (f i)))
⊢ IsIso f

Tactic:
change IsIso (isoMk X Y (fun i => asIso (f i))).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.GradedObject.isoMk, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
hf : ∀ (i : β), IsIso (f i)
⊢ IsIso (Iso.hom (X.isoMk Y fun (i : β) ↦ asIso (f i)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
inst_1 : IsIso f
i : β
change : IsIso (X := Functor.obj (eval i) X) (Functor.map (eval i) f)
⊢ IsIso (f i)

Tactic:
change IsIso ((eval i).map f)

Premises used: CategoryTheory.IsIso, CategoryTheory.GradedObject.eval, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
inst_1 : IsIso f
i : β
⊢ IsIso (X := Functor.obj (eval i) X) (Functor.map (eval i) f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.hom ≫ e.inv) j = 𝟙 (X j)
rw₁ : Eq.{v_1 + 1} (α := X j ⟶ X j) (𝟙 X j : X j ⟶ X j) (𝟙 (X j) : X j ⟶ X j)
rw₂ rw₃ : Eq.{v_1 + 1} (α := X j ⟶ X j) (𝟙 (X j)) (𝟙 (X j))
⊢ e.hom j ≫ e.inv j = 𝟙 (X j)

Tactic:
rw [← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id]

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.GradedObject.categoryOfGradedObjects_comp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
J : Type u_4
inst : Category.{v_1, u_1} C
X Y : GradedObject J C
e : X ≅ Y
j : J
rw : (e.inv ≫ e.hom) j = 𝟙 (Y j)
rw₁ : Eq.{v_1 + 1} (α := Y j ⟶ Y j) (𝟙 Y j : Y j ⟶ Y j) (𝟙 (Y j) : Y j ⟶ Y j)
rw₂ rw₃ : Eq.{v_1 + 1} (α := Y j ⟶ Y j) (𝟙 (Y j)) (𝟙 (Y j))
⊢ e.inv j ≫ e.hom j = 𝟙 (Y j)

Tactic:
rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.categoryOfGradedObjects_comp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
rw₁ : F.map ((e.hom ≫ e.inv) j) = 𝟙 (F.obj (X j))
rw₂ : F.map (𝟙 X j) = 𝟙 (F.obj (X j))
rw₃ : F.map (𝟙 (X j)) = 𝟙 (F.obj (X j))
rw₄ rw₅ : Eq.{v_2 + 1} (α := F.obj (X j) ⟶ F.obj (X j)) (𝟙 (F.obj (X j))) (𝟙 (F.obj (X j)))
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))

Tactic:
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.GradedObject.categoryOfGradedObjects_comp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
D : Type u_2
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J
rw : F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
rw₁ : F.map ((e.inv ≫ e.hom) j) = 𝟙 (F.obj (Y j))
rw₂ : F.map (𝟙 Y j) = 𝟙 (F.obj (Y j))
rw₃ : F.map (𝟙 (Y j)) = 𝟙 (F.obj (Y j))
rw₄ rw₅ : Eq.{v_2 + 1} (α := F.obj (Y j) ⟶ F.obj (Y j)) (𝟙 (F.obj (Y j))) (𝟙 (F.obj (Y j)))
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))

Tactic:
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
    GradedObject.categoryOfGradedObjects_id, Functor.map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.GradedObject.categoryOfGradedObjects_comp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₁ : (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₂ : (F.map (𝟙 (X j))).app Y = 𝟙 ((F.obj (X j)).obj Y)
rw₃ : NatTrans.app (𝟙 (F.obj (X j))) Y = 𝟙 ((F.obj (X j)).obj Y)
rw₄ rw₅ :
  Eq.{v_3 + 1} (α := (F.obj (X j)).obj Y ⟶ (F.obj (X j)).obj Y) (𝟙 ((F.obj (X j)).obj Y)) (𝟙 ((F.obj (X j)).obj Y))
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)

Tactic:
rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Iso.hom_inv_id_eval, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
X Y_1 : GradedObject J C
e : X ≅ Y_1
F : C ⥤ Functor.{v_2, v_3, u_2, u_3} D E
j : J
Y : D
rw : (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₁ : (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₂ : (F.map (𝟙 (Y_1 j))).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₃ : NatTrans.app (𝟙 (F.obj (Y_1 j))) Y = 𝟙 ((F.obj (Y_1 j)).obj Y)
rw₄ rw₅ :
  Eq.{v_3 + 1} (α := (F.obj (Y_1 j)).obj Y ⟶ (F.obj (Y_1 j)).obj Y) (𝟙 ((F.obj (Y_1 j)).obj Y))
    (𝟙 ((F.obj (Y_1 j)).obj Y))
⊢ (F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y_1 j)).obj Y)

Tactic:
rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval,
    Functor.map_id, NatTrans.id_app]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Iso.inv_hom_id_eval
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
subst : Eq.{v + 1} (α := x i ⟶ x i) (eqToHom ⋯ i : x i ⟶ x i) (eqToHom ⋯ : x i ⟶ x i)
⊢ Eq.{v + 1} (α := x i ⟶ x' i) (eqToHom h i : x i ⟶ x' i) (eqToHom ⋯ : x i ⟶ x' i)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ Eq.{v + 1} (α := x i ⟶ x i) (eqToHom ⋯ i : x i ⟶ x i) (eqToHom ⋯ : x i ⟶ x i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
dsimp : X (f b) = X (g b)
⊢ Functor.obj (comap C f) X b = Functor.obj (comap C g) X b

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)

Tactic:
simp only [h]
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
dsimp : X (g b) = X (f b)
⊢ Functor.obj (comap C g) X b = Functor.obj (comap C f) X b

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)

Tactic:
simp only [h]
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := Iso (C := GradedObject γ C ⥤ GradedObject β C) (comap C g) (comap C f)) (comapEq C ⋯)
    (Iso.symm (comapEq C h))
⊢ Eq (α := Iso (C := GradedObject γ C ⥤ GradedObject β C) (comap C g) (comap C f)) (comapEq C ⋯)
    (Iso.symm (comapEq C h))

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
rw rw₁ : Y b = Y b
⊢ X b = Y b

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
subst : Eq.{v + 1} (α := X b ⟶ X b) (eqToHom ⋯ b : X b ⟶ X b) (eqToHom ⋯ : X b ⟶ X b)
⊢ Eq.{v + 1} (α := X b ⟶ Y b) (eqToHom h b : X b ⟶ Y b) (eqToHom ⋯ : X b ⟶ Y b)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ Eq.{v + 1} (α := X b ⟶ X b) (eqToHom ⋯ b : X b ⟶ X b) (eqToHom ⋯ : X b ⟶ X b)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
h : ∀ (x : β), x = Function.comp (β := γ) (⇑e.symm : (a : γ) → β) (⇑e : (a : β) → γ) x
⊢ Eq (α := β → β) (fun (i : β) ↦ i) (Function.comp (β := γ) (⇑e.symm : (a : γ) → β) (⇑e : (a : β) → γ))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x : β
⊢ x = Function.comp (β := γ) (⇑e.symm : (a : γ) → β) (⇑e : (a : β) → γ) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
h : ∀ (x : γ), Function.comp (β := β) (⇑e : (a : β) → γ) (⇑e.symm : (a : γ) → β) x = x
⊢ Eq (α := γ → γ) (Function.comp (β := β) (⇑e : (a : β) → γ) (⇑e.symm : (a : γ) → β)) fun (i : γ) ↦ i

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x : γ
⊢ Function.comp (β := β) (⇑e : (a : β) → γ) (⇑e.symm : (a : γ) → β) x = x

Tactic:
simp