awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i k : D.J
⊢ Eq (α := pullback (D.f' i i) (D.f' i k) ⟶ if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' i k) (D.f' i i))
      (if hij : i = i then
        Iso.hom (pullbackSymmetry (D.f' i i) (D.f' i k)) ≫
          pullback.map (D.f' i k) (D.f' i i) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i i) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
        else
          if hjk : i = k then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
          else
            pullback.map (D.f' i i) (D.f' i k) (D.f i i hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i i k hij hik hjk ≫
                pullback.map (D.f i k hjk) (D.f i i ⋯) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' i k) (D.f' i i)))
    (pullback.fst (D.f' i i) (D.f' i k) ≫ if h : i = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i i h ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j : D.J
h : i ≠ j
⊢ Eq (α := pullback (D.f' i j) (D.f' i i) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' j i) (D.f' j i))
      (if hij : i = j then
        Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i i)) ≫
          pullback.map (D.f' i i) (D.f' i j) (D.f' j i) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = i then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i i) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j i) (D.f' j i))
        else
          if hjk : j = i then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j i) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i i) (D.f i j hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j i hij hik hjk ≫
                pullback.map (D.f j i hjk) (D.f j i ⋯) (D.f' j i) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' j i) (D.f' j i)))
    (pullback.fst (D.f' i j) (D.f' i i) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j : D.J
h h_1 : i ≠ j
⊢ Eq (α := pullback (D.f' i j) (D.f' i j) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' j j) (D.f' j i))
      (if hij : i = j then
        Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i j)) ≫
          pullback.map (D.f' i j) (D.f' i j) (D.f' j j) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = j then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i j) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j j) (D.f' j i))
        else
          if hjk : j = j then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i j) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j j) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i j) (D.f i j hij) (D.f i j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j j hij hik hjk ≫
                pullback.map (D.f j j hjk) (D.f j i ⋯) (D.f' j j) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' j j) (D.f' j i)))
    (pullback.fst (D.f' i j) (D.f' i j) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
h : i ≠ j
h_1 : i ≠ k
h_2 : j ≠ k
⊢ Eq (α := pullback (D.f' i j) (D.f' i k) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' j k) (D.f' j i))
      (if hij : i = j then
        Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i k)) ≫
          pullback.map (D.f' i k) (D.f' i j) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          if hjk : j = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i k) (D.f i j hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j k hij hik hjk ≫
                pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' j k) (D.f' j i)))
    (pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)

Tactic:
simp [*, reassoc_of% D.t_fac]

Premises used: CategoryTheory.GlueData'.t_fac
-- Module: Mathlib.CategoryTheory.GradedObject.Associator
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
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_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_5, u_6} C₃ C₄
F : C₁ ⥤ Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
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_12} r
ρ₂₃ : 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_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst_8 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_9 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
dsimp :
  Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
      (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j)
        (Iso.inv (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃) j)
        (CategoryStruct.comp (Y := (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).mapObj r j)
          (mapMap ((((mapTrifunctorMapNatTrans associator.hom I₁ I₂ I₃).app X₁).app X₂).app X₃) r j)
          (Iso.hom (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃) j))))
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
      (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (Iso.hom (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃) j))
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
dsimp [mapBifunctorAssociator]

Premises used: CategoryTheory.GradedObject.mapBifunctorAssociator
-- Module: Mathlib.CategoryTheory.GradedObject.Associator
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
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_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_5, u_6} C₃ C₄
F : C₁ ⥤ Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
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_12} r
ρ₂₃ : 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_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst_8 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_9 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
erw erw₁ :
  Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ (i₁, i₂, i₃).1)) (X₂ (i₁, i₂, i₃).2.1)) (X₃ (i₁, i₂, i₃).2.2) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j)
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ (i₁, i₂, i₃).1)) (X₂ (i₁, i₂, i₃).2.1)) (X₃ (i₁, i₂, i₃).2.2) ≫
      CategoryStruct.comp (Y := (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).mapObj r j)
        ((((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h)
        (Iso.hom (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃) j))
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

Tactic:
erw [ι_mapBifunctorComp₂₃MapObjIso_hom]

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
f : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
g : Y₁ ⟶ Y₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
i : I
j : J
k : K
h : p (i, j) = k
⊢ Eq (α := (F.obj (X₁ i)).obj (Y₁ j) ⟶ mapBifunctorMapObj F p X₂ Y₂ k)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁ k) (ιMapBifunctorMapObj F p X₁ Y₁ i j k h)
      (mapBifunctorMapMap F p f g k))
    ((F.map (f i)).app (Y₁ j) ≫ (F.obj (X₂ i)).map (g j) ≫ ιMapBifunctorMapObj F p X₂ Y₂ i j k h)

Tactic:
simp [ιMapBifunctorMapObj, mapBifunctorMapMap]

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapMap
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst_3 : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
hfg :
  ∀ (i : I × J) (hij : p i = k),
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ f =
      (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ g
⊢ f = g

Tactic:
apply mapObj_ext

Premises used: CategoryTheory.GradedObject.mapObj_ext
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst_3 : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
i : I
j : J
hij : p (i, j) = k
⊢ (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ f =
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ g

Tactic:
h i j hij

Premises used: CategoryTheory.GradedObject.ιMapBifunctorMapObj, CategoryTheory.GradedObject.mapBifunctorMapObj
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst_3 : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
i : I
j : J
hij : p (i, j) = k
⊢ (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ f =
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ g

Tactic:
exact h i j hij
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst_3 : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)
i : I
j : J
hij : p (i, j) = k
⊢ CategoryStruct.comp (Y := mapBifunctorMapObj F p X Y k) (ιMapBifunctorMapObj F p X Y i j k hij)
      (mapBifunctorMapObjDesc f) =
    f i j hij

Tactic:
apply ι_descMapObj

Premises used: CategoryTheory.GradedObject.ι_descMapObj
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
h :
  ∀ (x : K) (i : I) (j : J) (hij : p (i, j) = x),
    Eq (α := (F.obj (X₁ i)).obj (Y₁ j) ⟶ mapBifunctorMapObj F p X₁ Y₁ x)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁ x) (ιMapBifunctorMapObj F p X₁ Y₁ i j x hij)
        (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂) (mapBifunctorMapMap F p e.hom e'.hom)
          (mapBifunctorMapMap F p e.inv e'.inv) x))
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁ x) (ιMapBifunctorMapObj F p X₁ Y₁ i j x hij)
        (𝟙 (mapBifunctorMapObj F p X₁ Y₁) x))
⊢ CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂) (mapBifunctorMapMap F p e.hom e'.hom)
      (mapBifunctorMapMap F p e.inv e'.inv) =
    𝟙 (mapBifunctorMapObj F p X₁ Y₁)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x : K
i : I
j : J
hij : p (i, j) = x
⊢ Eq (α := (F.obj (X₁ i)).obj (Y₁ j) ⟶ mapBifunctorMapObj F p X₁ Y₁ x)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁ x) (ιMapBifunctorMapObj F p X₁ Y₁ i j x hij)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂) (mapBifunctorMapMap F p e.hom e'.hom)
        (mapBifunctorMapMap F p e.inv e'.inv) x))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁ x) (ιMapBifunctorMapObj F p X₁ Y₁ i j x hij)
      (𝟙 (mapBifunctorMapObj F p X₁ Y₁) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
h :
  ∀ (x : K) (i : I) (j : J) (hij : p (i, j) = x),
    Eq (α := (F.obj (X₂ i)).obj (Y₂ j) ⟶ mapBifunctorMapObj F p X₂ Y₂ x)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
        (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁) (mapBifunctorMapMap F p e.inv e'.inv)
          (mapBifunctorMapMap F p e.hom e'.hom) x))
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
        (𝟙 (mapBifunctorMapObj F p X₂ Y₂) x))
⊢ CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁) (mapBifunctorMapMap F p e.inv e'.inv)
      (mapBifunctorMapMap F p e.hom e'.hom) =
    𝟙 (mapBifunctorMapObj F p X₂ Y₂)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x : K
i : I
j : J
hij : p (i, j) = x
⊢ Eq (α := (F.obj (X₂ i)).obj (Y₂ j) ⟶ mapBifunctorMapObj F p X₂ Y₂ x)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
      (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₁) (mapBifunctorMapMap F p e.inv e'.inv)
        (mapBifunctorMapMap F p e.hom e'.hom) x))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₂ x) (ιMapBifunctorMapObj F p X₂ Y₂ i j x hij)
      (𝟙 (mapBifunctorMapObj F p X₂ Y₂) x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst_3 : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst_4 : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst_5 : IsIso f
inst_6 : IsIso g
⊢ IsIso (X := mapBifunctorMapObj F p X₁ Y₁) (Y := mapBifunctorMapObj F p X₂ Y₂) (mapBifunctorMapMap F p f g)

Tactic:
inferInstanceAs <| IsIso (mapBifunctorMapMapIso F p (asIso f) (asIso g)).hom

Premises used: _private.0.CategoryTheory.GradedObject.instIsIsoMapBifunctorMapMap._proof_1
-- Module: Mathlib.CategoryTheory.GradedObject.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
inst_3 : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
dsimp :
  Eq (α := mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂)
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₁ Y₂)
      (mapMap (((mapBifunctor F I J).map (𝟙 X₁)).app Y₁ ≫ ((mapBifunctor F I J).obj X₁).map ψ) p)
      (mapMap (((mapBifunctor F I J).map φ).app Y₂ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₂)) p))
    (CategoryStruct.comp (Y := mapBifunctorMapObj F p X₂ Y₁)
      (mapMap (((mapBifunctor F I J).map φ).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₁)) p)
      (mapMap (((mapBifunctor F I J).map (𝟙 X₂)).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map ψ) p))
⊢ Eq (α :=
    Quiver.Hom (V := GradedObject K C₃)
      (Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₁ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₁)
      (Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₂))
    (Functor.map
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₁ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
          map_comp := ⋯ : GradedObject J C₂ ⥤ GradedObject K C₃ }
        ψ ≫
      mapBifunctorMapMap F p φ (𝟙 Y₂))
    (CategoryStruct.comp (Y :=
      Functor.obj
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        Y₁)
      (mapBifunctorMapMap F p φ (𝟙 Y₁))
      (Functor.map
        { obj := fun (Y : GradedObject J C₂) ↦ mapBifunctorMapObj F p X₂ Y,
          map := fun {X Y : GradedObject J C₂} (ψ : X ⟶ Y) ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
          map_comp := ⋯ }
        ψ))

Tactic:
dsimp