awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ_1 : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ (F.obj X₁).map ((G₂₃.obj X₂).map φ) ≫ (F.obj X₁).map ((G₂₃.map φ_1).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ_1).app X₃) ≫ (F.obj X₁).map ((G₂₃.obj Y₂).map φ)

Tactic:
simp only [← Functor.map_comp, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
dsimp :
  (F.obj X₁).map ((G₂₃.obj X₂).map f) ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.obj X₂).map f)
⊢ (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂).map f ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
⊢ (F.obj X₁).map ((G₂₃.obj X₂).map f) ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.obj X₂).map f)

Tactic:
simp only [← Functor.map_comp, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
w :
  ∀ (X₃ : C₃),
    NatTrans.app
        (((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ })
        X₃ =
      NatTrans.app
        ({ app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ :
            NatTrans (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂) (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂) } ≫
          ((bifunctorComp₂₃ F G₂₃').obj X₁).map f)
        X₃
⊢ ((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫
      { app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ } =
    { app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ :
        NatTrans (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂) (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂) } ≫
      ((bifunctorComp₂₃ F G₂₃').obj X₁).map f

Tactic:
ext X₃
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
w :
  (F.obj X₁).map ((G₂₃.map f).app X₃) ≫ (F.obj X₁).map ((φ.app Y₂).app X₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.map f).app X₃)
⊢ NatTrans.app
      (((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫
        { app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ })
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ :
          NatTrans (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂) (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂) } ≫
        ((bifunctorComp₂₃ F G₂₃').obj X₁).map f)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (F.obj X₁).map ((G₂₃.map f).app X₃) ≫ (F.obj X₁).map ((φ.app Y₂).app X₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.map f).app X₃)

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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 F' : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
w :
  ∀ (X₂ : C₂) (X₃ : C₃),
    (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).map f ≫
                {
                  app := fun (X₂ : C₂) ↦
                    { app := fun (X₃ : C₃) ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
                      NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁).obj X₂)
                        (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁).obj X₂) },
                  naturality := ⋯ :
                  NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁)
                    ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁) }).app
            X₂).app
        X₃ =
      NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₂ : C₂) ↦
                { app := fun (X₃ : C₃) ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
                  NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁).obj X₂)
                    (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁).obj X₂) },
              naturality := ⋯ :
              NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁)
                ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁) } ≫
            (Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).map f)
          X₂)
        X₃
⊢ (Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).map f ≫
      {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁).obj X₂)
              (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁).obj X₂) },
        naturality := ⋯ :
        NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁)
          ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁) } =
    {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁).obj X₂)
              (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁).obj X₂) },
        naturality := ⋯ :
        NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁)
          ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁) } ≫
      (Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).map f

Tactic:
ext X₂ X₃
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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 F' : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
w :
  Eq (α := (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃) ⟶ (F'.obj Y₁).obj ((G₂₃.obj X₂).obj X₃))
    ((F.map f).app ((G₂₃.obj X₂).obj X₃) ≫ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃))
    ((φ.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫ (F'.map f).app ((G₂₃.obj X₂).obj X₃))
⊢ (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).map f ≫
              {
                app := fun (X₂ : C₂) ↦
                  { app := fun (X₃ : C₃) ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
                    NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁).obj X₂)
                      (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁).obj X₂) },
                naturality := ⋯ :
                NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁)
                  ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁) }).app
          X₂).app
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ :
                NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁).obj X₂)
                  (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁).obj X₂) },
            naturality := ⋯ :
            NatTrans ((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁)
              ((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁) } ≫
          (Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).map f)
        X₂)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
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 F' : C₁ ⥤ Functor.{v_6, v_4, u_6, u_4} C₂₃ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ Eq (α := (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃) ⟶ (F'.obj Y₁).obj ((G₂₃.obj X₂).obj X₃))
    ((F.map f).app ((G₂₃.obj X₂).obj X₃) ≫ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃))
    ((φ.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫ (F'.map f).app ((G₂₃.obj X₂).obj X₃))

Tactic:
simp only [← NatTrans.comp_app, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
α : TwoSquare T L R B
⊢ α.op.natTrans = NatTrans.op α.natTrans

Tactic:
rfl

Premises used: CategoryTheory.TwoSquare.op, rfl
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
α : TwoSquare T L R B
inst_4 : IsIso α.natTrans
⊢ IsIso α.op.natTrans

Tactic:
inferInstanceAs (IsIso (NatTrans.op α.natTrans))

Premises used: _private.0.CategoryTheory.TwoSquare.instIsIsoFunctorOppositeNatTransOp._proof_1
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
w w' : TwoSquare T L R B
h : ∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X
⊢ w = w'

Tactic:
NatTrans.ext (funext h)

Premises used: CategoryTheory.NatTrans.ext, funext, CategoryTheory.TwoSquare
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst_4 : Category.{v₅, u₅} C₅
inst_5 : Category.{v₆, u₆} C₆
inst_6 : Category.{v₇, u₇} C₇
inst_7 : Category.{v₈, u₈} C₈
T' : Functor.{v₂, v₅, u₂, u₅} C₂ C₅
R' : Functor.{v₅, v₆, u₅, u₆} C₅ C₆
B' : Functor.{v₄, v₆, u₄, u₆} C₄ C₆
L' : Functor.{v₃, v₇, u₃, u₇} C₃ C₇
R'' : Functor.{v₄, v₈, u₄, u₈} C₄ C₈
B'' : Functor.{v₇, v₈, u₇, u₈} C₇ C₈
C₉ : Type u₉
inst_8 : Category.{v₉, u₉} C₉
R₃ : Functor.{v₆, v₉, u₆, u₉} C₆ C₉
B₃ : Functor.{v₈, v₉, u₈, u₉} C₈ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
a : (B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))
| w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c))

Tactic:
rw [← Functor.comp_map _ B₃, ← w₄.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst_4 : Category.{v₅, u₅} C₅
inst_5 : Category.{v₆, u₆} C₆
inst_6 : Category.{v₇, u₇} C₇
inst_7 : Category.{v₈, u₈} C₈
T' : Functor.{v₂, v₅, u₂, u₅} C₂ C₅
R' : Functor.{v₅, v₆, u₅, u₆} C₅ C₆
B' : Functor.{v₄, v₆, u₄, u₆} C₄ C₆
L' : Functor.{v₃, v₇, u₃, u₇} C₃ C₇
R'' : Functor.{v₄, v₈, u₄, u₈} C₄ C₈
B'' : Functor.{v₇, v₈, u₇, u₈} C₇ C₈
C₉ : Type u₉
inst_8 : Category.{v₉, u₉} C₉
R₃ : Functor.{v₆, v₉, u₆, u₉} C₆ C₉
B₃ : Functor.{v₈, v₉, u₈, u₉} C₈ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
h :
  R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      ((B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))) ≫ B₃.map (w₃.natTrans.app (L.obj c))
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c)) ≫ B₃.map (w₃.natTrans.app (L.obj c))

Tactic:
slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Functor.TwoSquare
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} C₄
T : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L : Functor.{v₁, v₃, u₁, u₃} C₁ C₃
R : Functor.{v₂, v₄, u₂, u₄} C₂ C₄
B : Functor.{v₃, v₄, u₃, u₄} C₃ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst_4 : Category.{v₅, u₅} C₅
inst_5 : Category.{v₆, u₆} C₆
inst_6 : Category.{v₇, u₇} C₇
inst_7 : Category.{v₈, u₈} C₈
T' : Functor.{v₂, v₅, u₂, u₅} C₂ C₅
R' : Functor.{v₅, v₆, u₅, u₆} C₅ C₆
B' : Functor.{v₄, v₆, u₄, u₆} C₄ C₆
L' : Functor.{v₃, v₇, u₃, u₇} C₃ C₇
R'' : Functor.{v₄, v₈, u₄, u₈} C₄ C₈
B'' : Functor.{v₇, v₈, u₇, u₈} C₇ C₈
C₉ : Type u₉
inst_8 : Category.{v₉, u₉} C₉
R₃ : Functor.{v₆, v₉, u₆, u₉} C₆ C₉
B₃ : Functor.{v₈, v₉, u₈, u₉} C₈ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      ((B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))) ≫ B₃.map (w₃.natTrans.app (L.obj c))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
h : IsLimit (F := pair (F.obj X) (F.obj Y))
  (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} X Y)) (F.map prod.fst) (F.map prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit F prod.fst prod.snd (prodIsProd X Y)
h' : IsLimit (F := pair (F.obj X) (F.obj Y)) (Types.binaryProductCone (F.obj X) (F.obj Y)) :=
  Types.binaryProductLimit (F.obj X) (F.obj Y)
⊢ True

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
h : IsLimit (F := pair (F.obj X) (F.obj Y))
  (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} X Y)) (F.map prod.fst) (F.map prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit F prod.fst prod.snd (prodIsProd X Y)
h' : IsLimit (F := pair (F.obj X) (F.obj Y)) (Types.binaryProductCone (F.obj X) (F.obj Y)) :=
  Types.binaryProductLimit (F.obj X) (F.obj Y)
⊢ ∃ (W : F.Elements) (x : W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) X x) (x :
    W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y), True

Tactic:
exact ⟨⟨X ⨯ Y, (h'.conePointUniqueUpToIso h).hom ⟨x, y⟩⟩,
      ⟨prod.fst, ConcreteCategory.congr_hom (h'.conePointUniqueUpToIso_hom_comp h (.mk .left)) _⟩,
      ⟨prod.snd, ConcreteCategory.congr_hom (h'.conePointUniqueUpToIso_hom_comp h (.mk .right)) _⟩,
      by tauto⟩
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf_1 : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x = y
g : X ⟶ Y
hf :
  Eq (α := F.obj Y) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x : F.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x : F.obj Y)
hg : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x = y
h : IsLimit (Fork.ofι (P := F.obj (equalizer f g)) (F.map (equalizer.ι f g)) ⋯) :=
  isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
h' : IsLimit (F := parallelPair (F.map f) (F.map g)) (LimitCone.cone Types.equalizerLimit) :=
  LimitCone.isLimit Types.equalizerLimit
⊢ ∃ (W : F.Elements) (h : W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) X x),
    Eq (α := W ⟶ Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y)
      (h ≫
        Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          f hf_1)
      (h ≫
        Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          g hg)

Tactic:
exact ⟨⟨equalizer f g, (h'.conePointUniqueUpToIso h).hom ⟨x, hf⟩⟩,
      ⟨equalizer.ι f g, ConcreteCategory.congr_hom
        (h'.conePointUniqueUpToIso_hom_comp h .zero) ⟨x, hf⟩⟩,
      by ext; exact equalizer.condition f g⟩
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : C
x : F.obj X
U V : Over.{v, u} X
x_1 : U ⟶ V
x_2 : (Over.forget X ⋙ F).obj U
h :
  Membership.mem (γ := Set ((Over.forget X ⋙ F).obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj X))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map U.hom)) :
        (a : (fun (X : Type w) ↦ X) (F.obj U.left)) → (fun (X : Type w) ↦ X) (F.obj X))
      {x})
    x_2
⊢ Membership.mem (γ := Set ((Over.forget X ⋙ F).obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) ((Over.forget X ⋙ F).obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((Over.forget X ⋙ F).map x_1)) :
        (a : (fun (X : Type w) ↦ X) ((Over.forget X ⋙ F).obj U)) → (fun (X : Type w) ↦ X) ((Over.forget X ⋙ F).obj V))
      (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj X))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map V.hom)) :
          (a : (fun (X : Type w) ↦ X) (F.obj V.left)) → (fun (X : Type w) ↦ X) (F.obj X))
        {x}))
    x_2

Tactic:
simpa [← comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : C
x : F.obj X
U : Over.{v, u} X
u : F.obj U.left
⊢ u ∈ (fromOverSubfunctor F x).obj U ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map U.hom) :
          (a : (fun (X : Type w) ↦ X) (F.obj U.left)) → (fun (X : Type w) ↦ X) (F.obj X))
        u =
      x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton