awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫ ((θ ≫ ι).naturality f).hom =
    ((η ≫ ι).naturality f).hom ≫ Γ.as.app a ▷ ι.app a ▷ H.map f
have dsimp : F.map f ◁ Γ.as.app b ▷ ι.app b ≫
    (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
      (θ.naturality f).hom ▷ ι.app b ≫
        (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
          θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
  ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
    Γ.as.app a ▷ ι.app a ▷ H.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
have simp_rw : F.map f ◁ Γ.as.app b ▷ ι.app b ≫
    (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
      (θ.naturality f).hom ▷ ι.app b ≫
        (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
          θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
  (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
    (η.naturality f).hom ▷ ι.app b ≫
      (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
        Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
Tactic: simp_rw [Category.assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ
have w : ∀ (b_1 : B), (whiskerLeft f θ ≫ whiskerRight η i).as.app b_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app b_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g
have mk : ∀ (base : a.base ⟶ b.base) (fiber : (F.map base.toLoc).toFunctor.obj a.fiber ⟶ b.fiber)
  (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base)
  (hfg₂ : eqToHom sorry ≫ { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber),
  { base := base, fiber := fiber : a.Hom b } = g
Tactic: cases f
Cleared hypotheses: f, hfg₁, hfg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
g : a ⟶ b
base : a.base ⟶ b.base
fiber : (F.map base.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base
hfg₂ : eqToHom ⋯ ≫ { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber
⊢ { base := base, fiber := fiber : a.Hom b } = g
have mk : ∀ (base_1 : a.base ⟶ b.base) (fiber_1 : (F.map base_1.toLoc).toFunctor.obj a.fiber ⟶ b.fiber)
  (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = { base := base_1, fiber := fiber_1 }.base)
  (hfg₂ :
    eqToHom sorry ≫ { base := base, fiber := fiber : a.Hom b }.fiber =
      { base := base_1, fiber := fiber_1 : a.Hom b }.fiber),
  { base := base, fiber := fiber : a.Hom b } = { base := base_1, fiber := fiber_1 }
Tactic: cases g
Cleared hypotheses: g, hfg₁, hfg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
⊢ ∃ (hfg : f.base = g.base), eqToHom ⋯ ≫ f.fiber = g.fiber
have subst : ∃ (hfg : f.base = f.base), eqToHom sorry ≫ f.fiber = f.fiber
Tactic: subst hfg
Cleared hypotheses: g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber
have subst : f.fiber = eqToHom sorry ≫ f.fiber
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ 𝟙 a ≫ f = f
have hfg₁ : (𝟙 a ≫ f).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
hfg₁ : (𝟙 a ≫ f).base = f.base
⊢ 𝟙 a ≫ f = f
have hfg₂ : eqToHom sorry ≫ (𝟙 a ≫ f).fiber = f.fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ f ≫ 𝟙 b = f
have hfg₁ : (f ≫ 𝟙 b).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
hfg₁ : (f ≫ 𝟙 b).base = f.base
⊢ f ≫ 𝟙 b = f
have hfg₂ : eqToHom sorry ≫ (f ≫ 𝟙 b).fiber = f.fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W X Y Z : ∫ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have hfg₁ : ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W X Y Z : ∫ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
hfg₁ : ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have hfg₂ : eqToHom sorry ≫ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ { base := Hom.base (𝟙 a),
      fiber :=
        (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
          ∫ G } } =
    𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }
have hfg₁ : { base := Hom.base (𝟙 a),
      fiber :=
        (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
          ∫ G } }.base =
  Hom.base (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber })
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
hfg₁ :
  { base := Hom.base (𝟙 a),
        fiber :=
          (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G } }.base =
    Hom.base
      (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber })
⊢ { base := Hom.base (𝟙 a),
      fiber :=
        (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
          ∫ G } } =
    𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }
have hfg₂ : CategoryStruct.comp (Y :=
    (G.map
            { base := Hom.base (𝟙 a),
                  fiber :=
                    (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
                  { base := a.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                        ∫ G }.Hom
                    { base := a.base,
                      fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                      ∫ G } }.base.toLoc).toFunctor.obj
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }.fiber)
    (eqToHom sorry)
    { base := Hom.base (𝟙 a),
        fiber :=
          (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) }.fiber =
  Hom.fiber
    (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber : ∫ G })
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
      fiber :=
        (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
          ∫ G } } =
    { base := f.base,
        fiber :=
          (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
            ∫ G } } ≫
      { base := g.base,
        fiber :=
          (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber }
have hfg₁ : { base := (f ≫ g).base,
      fiber :=
        (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
          ∫ G } }.base =
  Hom.base
    ({ base := f.base,
        fiber :=
          (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
            ∫ G } } ≫
      { base := g.base,
        fiber :=
          (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber })
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ (map (𝟙 F)).map f = f
have hfg₁ : ((map (𝟙 F)).map f).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
hfg₁ : ((map (𝟙 F)).map f).base = f.base
⊢ (map (𝟙 F)).map f = f
have hfg₂ : eqToHom sorry ≫ ((map (𝟙 F)).map f).fiber = f.fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f ≫ Iso.hom ((fun (x : ∫ F) ↦ (eqToIso ⋯ : (map (α ≫ β)).obj x ≅ (map α ⋙ map β).obj x)) Y) =
    Iso.hom ((fun (x : ∫ F) ↦ (eqToIso ⋯ : (map (α ≫ β)).obj x ≅ (map α ⋙ map β).obj x)) X) ≫ (map α ⋙ map β).map f
have dsimp : (map (α ≫ β)).map f ≫ 𝟙 ((map (α ≫ β)).obj Y) = 𝟙 ((map (α ≫ β)).obj X) ≫ (map β).map ((map α).map f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f ≫ 𝟙 ((map (α ≫ β)).obj Y) = 𝟙 ((map (α ≫ β)).obj X) ≫ (map β).map ((map α).map f)
have simp : (map (α ≫ β)).map f = (map β).map ((map α).map f)
Tactic: simp only [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)
have hfg₁ : ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
hfg₁ : ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)
have hfg₂ : eqToHom sorry ≫ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : f.fiber = g.fiber ≫ eqToHom ⋯
⊢ f = g
have mk : ∀ (base : a.base ⟶ b.base) (fiber : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base.op.toLoc)) b.fiber)
  (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base)
  (hfg₂ : { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber ≫ eqToHom sorry),
  { base := base, fiber := fiber : a.Hom b } = g
Tactic: cases f
Cleared hypotheses: f, hfg₁, hfg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
g : a ⟶ b
base : a.base ⟶ b.base
fiber : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base.op.toLoc)) b.fiber
hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base
hfg₂ : { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base, fiber := fiber : a.Hom b } = g
have mk : ∀ (base_1 : a.base ⟶ b.base) (fiber_1 : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base_1.op.toLoc)) b.fiber)
  (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = { base := base_1, fiber := fiber_1 }.base)
  (hfg₂ :
    { base := base, fiber := fiber : a.Hom b }.fiber =
      { base := base_1, fiber := fiber_1 : a.Hom b }.fiber ≫ eqToHom sorry),
  { base := base, fiber := fiber : a.Hom b } = { base := base_1, fiber := fiber_1 }
Tactic: cases g
Cleared hypotheses: g, hfg₁, hfg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f g : a ⟶ b
hfg : f = g
⊢ f.base = g.base
have rw : g.base = g.base
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ 𝟙 a ≫ f = f
have hfg₁ : (𝟙 a ≫ f).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
hfg₁ : (𝟙 a ≫ f).base = f.base
⊢ 𝟙 a ≫ f = f
have hfg₂ : (𝟙 a ≫ f).fiber = f.fiber ≫ eqToHom sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ f ≫ 𝟙 b = f
have hfg₁ : (f ≫ 𝟙 b).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
hfg₁ : (f ≫ 𝟙 b).base = f.base
⊢ f ≫ 𝟙 b = f
have hfg₂ : (f ≫ 𝟙 b).fiber = f.fiber ≫ eqToHom sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
W X Y Z : ∫ᶜ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have hfg₁ : ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
W X Y Z : ∫ᶜ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
hfg₁ : ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have hfg₂ : ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber ≫ eqToHom sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := Hom.base (𝟙 a),
      fiber :=
        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (Hom.fiber (𝟙 a)) ≫
          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc))) a.fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
          ∫ᶜ G } } =
    𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber }
have hfg₁ : { base := Hom.base (𝟙 a),
      fiber :=
        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (Hom.fiber (𝟙 a)) ≫
          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc))) a.fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
          ∫ᶜ G } }.base =
  Hom.base
    (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber })
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
      fiber :=
        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (f ≫ g).fiber ≫
          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.Hom
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
          ∫ᶜ G } } =
    { base := f.base,
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.Hom
          { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber :
            ∫ᶜ G } } ≫
      { base := g.base,
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber }
have hfg₁ : { base := (f ≫ g).base,
      fiber :=
        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (f ≫ g).fiber ≫
          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.Hom
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
          ∫ᶜ G } }.base =
  Hom.base
    ({ base := f.base,
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.Hom
          { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber :
            ∫ᶜ G } } ≫
      { base := g.base,
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber })
Tactic: ext