awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : i = k
⊢ IsIso (X := pullback (D.f' j k) (D.f' j i)) (pullback.snd (D.f' j k) (D.f' j i))
have subst : IsIso (X := pullback (D.f' j i) (D.f' j i)) (pullback.snd (D.f' j i) (D.f' j i))
Tactic: subst hik
Cleared hypotheses: k, hik
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (X := pullback (D.f' j k) (D.f' j i)) (pullback.snd (D.f' j k) (D.f' j i))
have inst : IsIso (D.f' j k)
Tactic: apply +allowSynthFailures pullback_snd_iso_of_left_iso
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso (D.f' j k)
have inst : IsIso.{v, u₁} (eqToHom sorry)
Tactic: simp only [hjk, GlueData'.f', ↓reduceDIte]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then D.U i else D.V i k h) = D.V i k hik
have rw : D.V i k hik = D.V i k hik
Tactic: rw [dif_neg hik]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij
have delta : (if h : i = j then eqToHom sorry else eqToHom sorry ≫ D.f i j h) ≫ eqToHom sorry = eqToHom sorry ≫ D.f i j hij
Tactic: delta f'
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik
have delta : (if h : i = k then eqToHom sorry else eqToHom sorry ≫ D.f i k h) ≫ eqToHom sorry = eqToHom sorry ≫ D.f i k hik
Tactic: delta f'
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k
have delta : D.f j k hjk ≫ eqToHom sorry = eqToHom sorry ≫ if h : j = k then eqToHom sorry else eqToHom sorry ≫ D.f j k h
Tactic: delta f'
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i
have delta : D.f j i sorry ≫ eqToHom sorry = eqToHom sorry ≫ if h : j = i then eqToHom sorry else eqToHom sorry ≫ D.f j i h
Tactic: delta f'
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i : D.J
⊢ IsIso (D.f' i i)
have simp : IsIso.{v, u₁} (eqToHom sorry)
Tactic: simp only [↓reduceDIte, GlueData'.f']
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ D.t'' i j k ≫ 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 ⋯
have delta : 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
    else
      if hik : i = k then
        have this := sorry;
        pullback.fst (D.f' i j) (D.f' i k) ≫
          eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
      else
        if hjk : j = k then
          have this := sorry;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
            D.t' i j k hij hik hjk ≫
              pullback.map (D.f j k hjk) (D.f j i sorry) (D.f' j k) (D.f' j i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
    (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 sorry else eqToHom sorry ≫ D.t i j h ≫ eqToHom sorry)
Tactic: delta GlueData'.t''
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ 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 ⋯)
have inl : 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
    else
      if hik : i = k then
        have this := sorry;
        pullback.fst (D.f' i i) (D.f' i k) ≫
          eqToHom sorry ≫ D.t i i hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
      else
        if hjk : i = k then
          have this := sorry;
          pullback.fst (D.f' i i) (D.f' i k) ≫
            eqToHom sorry ≫ D.t i i hij ≫ eqToHom sorry ≫ 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
            D.t' i i k hij hik hjk ≫
              pullback.map (D.f i k hjk) (D.f i i sorry) (D.f' i k) (D.f' i i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
    (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 sorry else eqToHom sorry ≫ D.t i i h ≫ eqToHom sorry)
Tactic: obtain rfl | _ := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ 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 ⋯)
have inr : 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
    else
      if hik : i = i then
        have this := sorry;
        pullback.fst (D.f' i j) (D.f' i i) ≫
          eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' j i) (D.f' j i))
      else
        if hjk : j = i then
          have this := sorry;
          pullback.fst (D.f' i j) (D.f' i i) ≫
            eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
            D.t' i j i hij hik hjk ≫
              pullback.map (D.f j i hjk) (D.f j i sorry) (D.f' j i) (D.f' j i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
    (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 sorry else eqToHom sorry ≫ D.t i j h ≫ eqToHom sorry)
Tactic: obtain rfl | _ := eq_or_ne i k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ 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 ⋯)
have inr : 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
      else
        if hik : i = j then
          have this := sorry;
          pullback.fst (D.f' i j) (D.f' i j) ≫
            eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' j j) (D.f' j i))
        else
          if hjk : j = j then
            have this := sorry;
            pullback.fst (D.f' i j) (D.f' i j) ≫
              eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ 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 sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
              D.t' i j j hij hik hjk ≫
                pullback.map (D.f j j hjk) (D.f j i sorry) (D.f' j j) (D.f' j i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
      (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 sorry else eqToHom sorry ≫ D.t i j h ≫ eqToHom sorry)
Tactic: obtain rfl | _ := eq_or_ne j k
Cleared hypotheses: k, h_1
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Associator (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_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
⊢ 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)
have 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)
Tactic: dsimp [mapBifunctorAssociator]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Associator (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_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
⊢ 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)
have rw : 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: rw [ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ιMapTrifunctorMapObj,
    ι_mapMap_assoc, mapTrifunctorMapNatTrans_app_app_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Associator (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_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
⊢ 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)
have 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)
Tactic: erw [ι_mapBifunctorComp₂₃MapObjIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Bifunctor (goal)
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
⊢ f = g
have 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
Tactic: apply mapObj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Bifunctor (goal)
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₂
⊢ 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₁)
have 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))
Tactic: ext