awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₁₂ F₁₂' : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
f : G ⟶ G'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ Eq (α :=
    (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂).obj X₃ ⟶
      (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G').obj X₁).obj X₂).obj X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
            {
              app := fun (X₁ : C₁) ↦
                {
                  app := fun (X₂ : C₂) ↦
                    { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                  naturality := ⋯ },
              naturality := ⋯ })
          X₁)
        X₂)
      X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₁ : C₁) ↦
                { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                  naturality := ⋯ },
              naturality := ⋯ } ≫
            Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)
          X₁)
        X₂)
      X₃)
have w : NatTrans.app (f.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((φ.app X₁).app X₂)).app X₃ =
  (G.map ((φ.app X₁).app X₂)).app X₃ ≫ NatTrans.app (f.app ((F₁₂'.obj X₁).obj X₂)) X₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ_1 : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ Eq.{v_4 + 1} (α :=
    Quiver.Hom.{v_4, u_4} (V := C₄)
      (Functor.obj.{v_3, v_4, u_3, u_4}
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ), map_id := ⋯, map_comp := ⋯ }
        X₃)
      (Functor.obj.{v_3, v_4, u_3, u_4}
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ), map_id := ⋯, map_comp := ⋯ }
        Y₃))
    (Functor.map
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ), map_id := ⋯, map_comp := ⋯ }
        φ ≫
      (F.obj X₁).map ((G₂₃.map φ_1).app Y₃))
    ((F.obj X₁).map ((G₂₃.map φ_1).app X₃) ≫
      Functor.map
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ), map_id := ⋯, map_comp := ⋯ }
        φ)
have dsimp : (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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₂₃ 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₃
⊢ (((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
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₂₃ G₂₃' : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((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
have 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 := sorry })
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := sorry :
          NatTrans (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂) (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂) } ≫
        ((bifunctorComp₂₃ F G₂₃').obj X₁).map f)
      X₃
Tactic: ext X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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₂₃ 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₃
⊢ 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₃
have 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₃)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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 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₁
⊢ (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
have 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 := sorry :
                    NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj Y₁).obj X₂)
                      (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj Y₁).obj X₂) },
                naturality := sorry :
                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 := sorry :
                NatTrans (((Functor.obj (bifunctorComp₂₃FunctorObj F) G₂₃).obj X₁).obj X₂)
                  (((Functor.obj (bifunctorComp₂₃FunctorObj F') G₂₃).obj X₁).obj X₂) },
            naturality := sorry :
            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: ext X₂ X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.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 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₃
⊢ (((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₃
have 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₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TwoSquare (goal)
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₁
| w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c))
have a : (B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))
Tactic: rw [← Functor.comp_map _ B₃, ← w₄.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TwoSquare (goal)
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)) ≫
      w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c)) ≫ B₃.map (w₃.natTrans.app (L.obj c))
have 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))
Tactic: slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TypeValuedFlat (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X_1 : C
x : F.obj X_1
X : (fromOverFunctor F x).Elements
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp_all : Eq (α :=
  Quiver.Hom (V := Over (F.elementsMk X_1 x))
    (Over.mk
      (homMk
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
        sorry))
    (Over.mk
      (homMk
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
        sorry)))
  (Over.homMk
    (homMk
      (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
        (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
      (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
        (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
      (𝟙 X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left) sorry)
    sorry)
  (𝟙
    (Over.mk
      (homMk
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
        sorry)))
Tactic: simp_all
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : Finite G
⊢ HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C
have obtain : ∀ (G' : Type u₂) (hg : Group G') (hf : Fintype G') (e : G ≃* G'), HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C
Tactic: obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
G : Type u_1
inst_3 : Group G
inst_4 : Finite G
⊢ PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F
have choose : ∀ (G' : Type u₂) (hg : Group G') (hf : Fintype G') (he : Nonempty (G ≃* G')),
  PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F
Tactic: choose G' hg hf he using Finite.exists_type_univ_nonempty_mulEquiv G
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
h : Mono (F.map f)
⊢ Mono f
have this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
Tactic: haveI : IsIso (pullback.fst (F.map f) (F.map f)) :=
    isIso_fst_of_mono (F.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
⊢ IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
have rw : IsIso (X := F.obj (pullback f f))
  (CategoryStruct.comp (Y := pullback (F.map f) (F.map f)) (Iso.hom (PreservesPullback.iso F f f))
    (pullback.fst (F.map f) (F.map f)))
Tactic: rw [← PreservesPullback.iso_hom_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
⊢ Mono f
have this₁ : IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
Tactic: haveI : IsIso (F.map (pullback.fst f f)) := by
    rw [← PreservesPullback.iso_hom_fst]
    exact IsIso.comp_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
h : Mono (F.map f)
this_1 : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
this : IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
⊢ Mono f
have this₁ : IsIso (X := pullback f f) (pullback.fst f f)
Tactic: haveI : IsIso (pullback.fst f f) := isIso_of_reflects_iso (pullback.fst _ _) F
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
⊢ f = g
have this : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
Tactic: haveI : IsIso (equalizer.ι (F.map f) (F.map g)) := equalizer.ι_of_eq h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
have rw : IsIso (X := F.obj (equalizer f g))
  (CategoryStruct.comp (Y := equalizer (F.map f) (F.map g)) (equalizerComparison f g F)
    (equalizer.ι (F.map f) (F.map g)))
Tactic: rw [← equalizerComparison_comp_π f g F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
⊢ f = g
have this₁ : IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
Tactic: haveI : IsIso (F.map (equalizer.ι f g)) := by
      rw [← equalizerComparison_comp_π f g F]
      exact IsIso.comp_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this_1 : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
this : IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
⊢ f = g
have this₁ : IsIso (X := equalizer f g) (equalizer.ι f g)
Tactic: haveI : IsIso (equalizer.ι f g) := isIso_of_reflects_iso _ F
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
hc : ¬IsConnected.{u₁, u₂} X
hi : ∀ (a : IsInitial.{u₂, u₁} X), False
⊢ ∃ (Y : C) (v : Y ⟶ X), (∀ (a : IsInitial.{u₂, u₁} Y), False) ∧ Mono v ∧ ¬IsIso v
have contrapose! : ∀ (hc : ∀ (Y : C) (v : Y ⟶ X) (_ : ∀ (a : IsInitial.{u₂, u₁} Y), False) (_ : Mono v), IsIso v), IsConnected.{u₁, u₂} X
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X Y : C
i : X ≅ Y
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
have have : ∀ (e : (F.obj X).obj ≃ (F.obj Y).obj), Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
Tactic: have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : C
⊢ Nonempty (IsInitial.{u₂, u₁} X) ↔ IsEmpty.{w + 1} (F.obj X).obj
have rw : Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj
Tactic: rw [(IsInitial.isInitialIffObj F X).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : C
⊢ Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj
have this : PreservesFiniteColimits
  (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
Tactic: haveI : PreservesFiniteColimits (forget FintypeCat) := by
    change PreservesFiniteColimits FintypeCat.incl
    infer_instance