awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      ((mapTrifunctorMapFunctorObj F p X₁).map ψ ≫
        { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃), naturality := ⋯ })
      X₃ j)
    (NatTrans.app
      ({ app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃), naturality := ⋯ :
          NatTrans ((mapTrifunctorMapFunctorObj F p X₁).obj X₂) ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂) } ≫
        (mapTrifunctorMapFunctorObj F p Y₁).map ψ)
      X₃ j)
have w : Eq (α := mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
  (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
    (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j))
  (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
    (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
⊢ Eq (α := mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
      (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
      (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j))
have w : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
        (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j)))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j)))
Tactic: ext i₁ i₂ i₃ h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
have rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
Tactic: rw [← h, ← ρ₁₂.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
have rw₁ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
Tactic: rw [← h, ← ρ₁₂.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ ρ₁₂.q (i₁₂, i₃) = j
have rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
Tactic: rw [← h₁₂, ← h, ← ρ₁₂.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
⊢ ρ₁₂.q (i₁₂, i₃) = j
have rw₁ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
Tactic: rw [← h₁₂, ← h, ← ρ₁₂.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
rw₁ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
⊢ ρ₁₂.q (i₁₂, i₃) = j
have rw₂ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
Tactic: rw [← h₁₂, ← h, ← ρ₁₂.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
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_5, u_5} C₁₂
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_6 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
    (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (NatTrans.app (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)) (X₃ i₃) ≫
      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
have subst : Eq (α :=
  (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
    mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
  (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
  (NatTrans.app (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ (ρ₁₂.p (i₁, i₂)) sorry)) (X₃ i₃) ≫
    ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ (ρ₁₂.p (i₁, i₂)) i₃ j sorry)
Tactic: subst h₁₂
Cleared hypotheses: i₁₂, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
have have : (h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)) → IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
Tactic: have h₁₂ : ∀ i₁₂, IsColimit (c₁₂ i₁₂) := fun i₁₂ =>
    (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).isColimitCofanMapObj ρ₁₂.p i₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
have have : (hc : IsColimit c) → IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
Tactic: have hc : IsColimit c := (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj
    (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).isColimitCofanMapObj ρ₁₂.q j
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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_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
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) →
  Cocone (J := Discrete (↑(ρ₁₂.p ⁻¹' {(↑i : ρ₁₂.I₁₂ × I₃).1}) : Type (max u_7 u_8)))
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i : ρ₁₂.I₁₂ × I₃).1) ⋙
      G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)) :=
  fun (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) ↦
    (G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)).mapCocone (c₁₂ (↑i : ρ₁₂.I₁₂ × I₃).1)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
have have : (hc₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) → IsColimit (c₁₂' i)) →
  IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
Tactic: have hc₁₂' : ∀ i, IsColimit (c₁₂' i) := fun i => isColimitOfPreserves _ (h₁₂ i.1.1)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
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_5, u_5} C₁₂
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_6 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj 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 (α :=
    (((bifunctorComp₁₂ F₁₂ G).obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
      mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ 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))
    (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
have dsimp : Eq (α :=
  (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
    mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ 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₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j))))
  (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
Tactic: dsimp [mapBifunctorComp₁₂MapObjIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
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_5, u_5} C₁₂
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} 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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_6 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
A : C₄
f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g
have h₁ : ∀ (i : (↑(r ⁻¹' {j}) : Type (max (max u_7 u_8) u_9))),
  Cofan.inj (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) i ≫ f =
    Cofan.inj (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) i ≫ g
Tactic: apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : 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_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = j
have rw : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = r (i₁, i₂, i₃)
Tactic: rw [← h, ← ρ₂₃.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : 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_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
rw : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = r (i₁, i₂, i₃)
⊢ ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = j
have rw₁ : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = ρ₂₃.q ((i₁, i₂, i₃).1, ρ₂₃.p (i₁, i₂, i₃).2)
Tactic: rw [← h, ← ρ₂₃.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : 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_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
⊢ ρ₂₃.q (i₁, i₂₃) = j
have rw : ρ₂₃.q (i₁, i₂₃) = r (i₁, i₂, i₃)
Tactic: rw [← h, ← h₂₃, ← ρ₂₃.hpq]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : 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_6 : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst_7 : (Functor.obj (Functor.obj (mapBifunctor F I₁ ρ₂₃.I₂₃) X₁) (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
rw : ρ₂₃.q (i₁, i₂₃) = r (i₁, i₂, i₃)
⊢ ρ₂₃.q (i₁, i₂₃) = j
have rw₁ : ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = r (i₁, i₂, i₃)
Tactic: rw [← h, ← h₂₃, ← ρ₂₃.hpq]