awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
x : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
      { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } } =
    𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber }
have w_fiber : CategoryStruct.comp (Y :=
    (F.map
            { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
                { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
                  { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base).toFunctor.obj
      { base := x.base, fiber := obj AsSmall.down x.fiber }.fiber)
    (eqToHom sorry) { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) }.fiber =
  Hom.fiber (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F })
Tactic: apply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
x : Grothendieck (F ⋙ Cat.asSmallFunctor)
w_fiber :
  CategoryStruct.comp (Y :=
      (F.map
              { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
                  { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
                    { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base).toFunctor.obj
        { base := x.base, fiber := obj AsSmall.down x.fiber }.fiber)
      (eqToHom ⋯) { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) }.fiber =
    Hom.fiber (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F })
⊢ { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
      { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } } =
    𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber }
have w_base : { base := Hom.base (𝟙 x), fiber := Functor.map AsSmall.down (Hom.fiber (𝟙 x)) :
      { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F }.Hom
        { base := x.base, fiber := obj AsSmall.down x.fiber : Grothendieck F } }.base =
  Hom.base (𝟙 { base := x.base, fiber := obj AsSmall.down x.fiber })
Tactic: apply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
⊢ (map (whiskerRight α Cat.asSmallFunctor)).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
            (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
              (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
          Y) =
    Iso.hom
        ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
            (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
              (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
          X) ≫
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f
have w_base : Hom.base
    ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
            (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
              (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
          Y)) =
  Hom.base
    (Iso.hom
        ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
            (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
              (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
          X) ≫
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f)
Tactic: fapply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (CategoryStruct.comp (Y :=
      obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))) (eqToHom ⋯)
      (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down) ≫ eqToHom ⋯))
have w_fiber : HEq (α :=
  Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
    (obj AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.obj
        (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
    (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
  (Functor.map AsSmall.up
    ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
  (β :=
  Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
    (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
    (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
  (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))
Tactic: simp only [conj_eqToHom_iff_heq']
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
⊢ HEq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (β :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
      (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))
have w_fiber : HEq (α :=
  Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
    (obj AsSmall.up
      ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj
        (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
    (obj AsSmall.up ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
  (Functor.map AsSmall.up
    ((Cat.Hom.toFunctor (𝟙 (G.obj Y.base))).map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
  (β :=
  Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
    (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down)))
    (obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down)))
  (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down))
Tactic: rw [G.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F_1 : C ⥤ Cat
E : Cat
F : (↑E : Type u) ⥤ Cat
⊢ Over.homMk (map (𝟙 F)).toCatHom ⋯ = 𝟙 (Over.mk (forget F).toCatHom)
have h : Cat.Hom.toFunctor (Over.Hom.left (Over.homMk (map (𝟙 F)).toCatHom sorry)) =
  (Over.Hom.left (𝟙 (Over.mk (forget F).toCatHom))).toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
E : Cat
X Y Z : (↑E : Type u) ⥤ Cat
α : X ⟶ Y
β : Y ⟶ Z
⊢ Eq (α := Over.mk (forget X).toCatHom ⟶ Over.mk (forget Z).toCatHom) (Over.homMk (map (α ≫ β)).toCatHom ⋯)
    (CategoryStruct.comp (Y := Over.mk (forget Y).toCatHom) (Over.homMk (map α).toCatHom ⋯)
      (Over.homMk (map β).toCatHom ⋯))
have simp : Eq (α := Over.mk (forget X).toCatHom ⟶ Over.mk (forget Z).toCatHom) (Over.homMk (map α ⋙ map β).toCatHom sorry)
  (CategoryStruct.comp (Y := Over.mk (forget Y).toCatHom) (Over.homMk (map α).toCatHom sorry)
    (Over.homMk (map β).toCatHom sorry))
Tactic: simp [Grothendieck.map_comp_eq α β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
X : Grothendieck (G ⋙ typeToCat)
⊢ obj (𝟭 (Grothendieck (G ⋙ typeToCat))) X ≅ (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X
have rcases : (base : C) →
  (as : G.obj base) →
    obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base, fiber := { as := as : Discrete (G.obj base) } } ≅
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj
        { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) }
Tactic: rcases X with ⟨_, ⟨⟩⟩
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
X : G.Elements
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X
have mk : (fst : C) →
  (snd : G.obj fst) →
    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
        (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ≅
      obj (𝟭 G.Elements) (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
fst : C
snd : G.obj fst
fst_1 : C
snd_1 : G.obj fst_1
f :
  (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)
e :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
        (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c)
⊢ (grothendieckTypeToCatFunctor G).map
        ((grothendieckTypeToCatInverse G).map
          (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) ≫
      𝟙
        ((grothendieckTypeToCatFunctor G).obj
          ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1))) =
    𝟙
        ((grothendieckTypeToCatFunctor G).obj
          ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))) ≫
      Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e
have simp : (grothendieckTypeToCatFunctor G).map
    ((grothendieckTypeToCatInverse G).map
      (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) =
  Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G H : Functor.{v₁, v, u₁, u} D C
α : G ≅ H
X Y : Grothendieck (G ⋙ F)
f : X ⟶ Y
⊢ (pre F G).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          Y) =
    Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          X) ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f
have w_base : Hom.base
    ((pre F G).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          Y)) =
  Hom.base
    (Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          X) ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f)
Tactic: fapply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G H : Functor.{v₁, v, u₁, u} D C
α : G ≅ H
X Y : Grothendieck (G ⋙ F)
f : X ⟶ Y
w_base :
  Hom.base
      ((pre F G).map f ≫
        Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            Y)) =
    Hom.base
      (Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            X) ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f)
⊢ (pre F G).map f ≫
      Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          Y) =
    Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          X) ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f
have w_fiber : eqToHom sorry ≫
    Hom.fiber
      ((pre F G).map f ≫
        Iso.hom
          ((fun (X : Grothendieck (G ⋙ F)) ↦
              ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
            Y)) =
  Hom.fiber
    (Iso.hom
        ((fun (X : Grothendieck (G ⋙ F)) ↦
            ({ base := G.obj X.base, fiber := X.fiber : Grothendieck F }.transportIso (α.app X.base)).symm)
          X) ≫
      (map (whiskerRight α.hom F) ⋙ pre F H).map f)
Tactic: fapply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) ≅ pre F G.functor ⋙ preInv F G
have refine : 𝟭 (Grothendieck (G.functor ⋙ F)) =
  map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))
Tactic: refine (eqToIso ?_)
      ≪≫ (Grothendieck.preUnitIso F G |> isoWhiskerLeft (map _))
      ≪≫ (pre_comp_map_assoc G.functor _ _ |> Eq.symm |> eqToIso)
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))
have _ : map (𝟙 (G.functor ⋙ F)) =
  map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))
Tactic: calc
      _ = map (𝟙 _) := map_id_eq.symm
      _ = map _ := ?_
      _ = map _ ⋙ map _ := map_comp_eq _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
⊢ map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))
have e_α : 𝟙 (G.functor ⋙ F) = G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
⊢ 𝟙 (G.functor ⋙ F) = G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)
have e_α : ∀ (X : D),
  (NatTrans.app (𝟙 (G.functor ⋙ F)) X).toFunctor =
    ((G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)).app X).toFunctor
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
⊢ CategoryStruct.comp (Y := (pre F G.functor).obj ((preInv F G).obj ((pre F G.functor).obj X)))
      ((pre F G.functor).map
          ((eqToIso ⋯ ≪≫
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).isoWhiskerLeft
                      (Grothendieck.preUnitIso F G) ≪≫
                    eqToIso ⋯).hom.app
            X) :
        (pre F G.functor).obj X ⟶ (pre F G.functor).obj ((preInv F G).obj ((pre F G.functor).obj X)))
      ((preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) :
        (preInv F G ⋙ pre F G.functor).obj ((pre F G.functor).obj X) ⟶
          obj (𝟭 (Grothendieck F)) ((pre F G.functor).obj X)) =
    𝟙 ((pre F G.functor).obj X)
have simp : (pre F G.functor).map
      (eqToHom sorry ≫
        ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
            X ≫
          NatTrans.app
            (𝟙 (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
            X) ≫
    (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
  𝟙 ((pre F G.functor).obj X)
Tactic: simp only [preInv, Grothendieck.preUnitIso, pre_id,
      Iso.trans_hom, eqToIso.hom, eqToHom_app, eqToHom_refl, isoWhiskerLeft_hom, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
⊢ (pre F G.functor).map
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            NatTrans.app
              (𝟙
                (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                  pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)
have w_base : Hom.base
    ((pre F G.functor).map
        (eqToHom sorry ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            NatTrans.app
              (𝟙
                (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                  pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)) =
  Hom.base (𝟙 ((pre F G.functor).obj X))
Tactic: fapply Grothendieck.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G_1 : Functor.{v, w, u, w + 1} C (Type w)
G : Equivalence.{v₁, v, u₁, u} D C
X : Grothendieck (G.functor ⋙ F)
w_base :
  Hom.base
      ((pre F G.functor).map
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              NatTrans.app
                (𝟙
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                    pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)) =
    Hom.base (𝟙 ((pre F G.functor).obj X))
⊢ (pre F G.functor).map
        (eqToHom ⋯ ≫
          ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                  (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
              X ≫
            NatTrans.app
              (𝟙
                (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                  pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
              X) ≫
      (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
    𝟙 ((pre F G.functor).obj X)
have w_fiber : CategoryStruct.comp (Y :=
    obj.{v₂, v₂, u₂, u₂}
      (Cat.Hom.toFunctor
        (F.map
          (Hom.base
            ((pre F G.functor).map
                (eqToHom sorry ≫
                  ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                          (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                      X ≫
                    NatTrans.app
                      (𝟙
                        (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                          pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                      X) ≫
              (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)))))
      ((pre F G.functor).obj X).fiber)
    (eqToHom sorry)
    (Hom.fiber
      ((pre F G.functor).map
          (eqToHom sorry ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              NatTrans.app
                (𝟙
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                    pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)))
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X))) =
  Hom.fiber (𝟙 ((pre F G.functor).obj X))
Tactic: fapply Grothendieck.ext