awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ (homCartesianLift f g φ' ≫ cartesianLift a f).base = φ'.base

Tactic:
simpa using IsHomLift.fac (forget F) (g ≫ f) φ'

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.CoGrothendieck.forget, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ (homCartesianLift f g φ' ≫ cartesianLift a f).fiber = φ'.fiber ≫ eqToHom ⋯

Tactic:
simp [← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ homCartesianLift f g φ' ≫ cartesianLift a f = φ'

Tactic:
exact Hom.ext _ _ (by simpa using IsHomLift.fac (forget F) (g ≫ f) φ')
        (by simp [← Cat.Hom₂.comp_app])

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ g = χ'.base

Tactic:
simpa using IsHomLift.fac (forget F) g χ'

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.forget, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
refine_2 :
  ∀ (hχ'.symm : (forget F).IsHomLift χ'.base χ') (hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)),
    χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f g (χ' ≫ cartesianLift a f)

Tactic:
obtain ⟨rfl⟩ : g = χ'.1 := by simpa using IsHomLift.fac (forget F) g χ'

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.base, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
refine_2 : χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base
refine_2₁ : χ'.fiber = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).fiber ≫ eqToHom ⋯
⊢ χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base

Tactic:
simp [← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ'.fiber = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).fiber ≫ eqToHom ⋯

Tactic:
simp [← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
⊢ (forget F).IsFibered

Tactic:
IsFibered.of_exists_isStronglyCartesian (fun a _ f ↦
    ⟨domainCartesianLift a.2 f, cartesianLift a.2 f, isStronglyCartesian_homCartesianLift a.2 f⟩)

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift, CategoryTheory.Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift, CategoryTheory.Pseudofunctor.CoGrothendieck.fiber, CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian, Exists.intro, CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
φ : a ⟶ b
ψ : b ⟶ c
⊢ Eq.{v_1 + 1} (α := { base := S, fiber := a : ∫ᶜ F }.base ⟶ { base := S, fiber := c : ∫ᶜ F }.base)
    (Hom.base
      { base := 𝟙 S,
        fiber :=
          (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
    (Hom.base
      (CategoryStruct.comp (Y := { base := S, fiber := b })
        { base := 𝟙 S,
          fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
        { base := 𝟙 S,
          fiber := ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
φ : a ⟶ b
ψ : b ⟶ c
⊢ Eq.{u_3 + 1} (α :=
    { base := S, fiber := a : ∫ᶜ F }.fiber ⟶
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  { base := 𝟙 S,
                    fiber :=
                      (φ ≫ ψ) ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c :
                    { base := S, fiber := a : ∫ᶜ F }.Hom { base := S, fiber := c : ∫ᶜ F } })))))
        { base := S, fiber := c : ∫ᶜ F }.fiber)
    (Hom.fiber
      { base := 𝟙 S,
        fiber :=
          (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
    (CategoryStruct.comp (Y :=
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  (CategoryStruct.comp (Y := { base := S, fiber := b : ∫ᶜ F })
                    { base := 𝟙 S,
                      fiber :=
                        φ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            b :
                      { base := S, fiber := a : ∫ᶜ F }.Hom { base := S, fiber := b : ∫ᶜ F } }
                    { base := 𝟙 S,
                      fiber :=
                        ψ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            c :
                      { base := S, fiber := b : ∫ᶜ F }.Hom { base := S, fiber := c : ∫ᶜ F } }))))))
        { base := S, fiber := c : ∫ᶜ F }.fiber)
      (Hom.fiber
        (CategoryStruct.comp (Y := { base := S, fiber := b })
          { base := 𝟙 S,
            fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
          { base := 𝟙 S,
            fiber :=
              ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }))
      (eqToHom ⋯))

Tactic:
simp [← (F.mapId ⟨op S⟩).inv.toNatTrans.naturality_assoc ψ, F.whiskerRight_mapId_inv_app,
        Strict.leftUnitor_eqToIso, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.LocallyDiscrete.mk, CategoryTheory.Pseudofunctor.mapId, Opposite.op, CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
⊢ ι F S ⋙ forget F = obj (const (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)) S

Tactic:
Functor.ext_of_iso (compIso F S) (fun _ ↦ rfl) (fun _ => rfl)

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.compIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)

Tactic:
simpa using (IsHomLift.fac (forget F) (𝟙 S) (fiberInclusion.map f)).symm

Premises used: CategoryTheory.Functor.Fiber.fiberInclusion, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, Eq.symm, CategoryTheory.Pseudofunctor.CoGrothendieck.forget, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)

Tactic:
have hf : (fiberInclusion.map f).base = 𝟙 S := by
      simpa using (IsHomLift.fac (forget F) (𝟙 S) (fiberInclusion.map f)).symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
⊢ obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber =
    (F.map (𝟙 { as := op S : LocallyDiscrete 𝒮ᵒᵖ })).toFunctor.obj Y

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
h :
  (Fiber.inducedFunctor ⋯).map
      (CategoryStruct.comp (Y :=
        obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
          (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
        (Hom.fiber (Functor.map fiberInclusion f))
        (eqToHom ⋯ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)) =
    f
⊢ ∃ (a : X ⟶ Y), (Fiber.inducedFunctor ⋯).map a = f

Tactic:
use (fiberInclusion.map f).fiber ≫ eqToHom (by simp [hf]) ≫
      (F.mapId ⟨op S⟩).hom.toNatTrans.app Y

Premises used: CategoryTheory.LocallyDiscrete.mk, CategoryTheory.Pseudofunctor.mapId, CategoryTheory.eqToHom, CategoryTheory.Functor.Fiber.fiberInclusion, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.fiber, CategoryTheory.Functor.map, Opposite.op, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
⊢ Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base
      (Functor.map fiberInclusion
        ((Fiber.inducedFunctor ⋯).map
          (CategoryStruct.comp (Y :=
            obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
              (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
            (Hom.fiber (Functor.map fiberInclusion f))
            (eqToHom ⋯ ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)))))
    (Hom.base (Functor.map fiberInclusion f))

Tactic:
simp [hf, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
⊢ Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).fiber ⟶
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  (Functor.map fiberInclusion
                    ((Fiber.inducedFunctor ⋯).map
                      (CategoryStruct.comp (Y :=
                        obj
                          (Cat.Hom.toFunctor
                            (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
                          (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
                        (Hom.fiber (Functor.map fiberInclusion f))
                        (eqToHom ⋯ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            Y)))))))))
        (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
    (Hom.fiber
      (Functor.map fiberInclusion
        ((Fiber.inducedFunctor ⋯).map
          (CategoryStruct.comp (Y :=
            obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
              (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
            (Hom.fiber (Functor.map fiberInclusion f))
            (eqToHom ⋯ ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)))))
    (CategoryStruct.comp (Y :=
      obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
        (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
      (Hom.fiber (Functor.map fiberInclusion f)) (eqToHom ⋯))

Tactic:
simp [hf, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f g : a ⟶ b
heq : (Fiber.inducedFunctor ⋯).map f = (Fiber.inducedFunctor ⋯).map g
⊢ Eq (α := obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj a) ⟶ obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj b))
    (Functor.map fiberInclusion ((Fiber.inducedFunctor ⋯).map f))
    (Functor.map fiberInclusion ((Fiber.inducedFunctor ⋯).map g))

Tactic:
replace heq := fiberInclusion.congr_map heq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f g : a ⟶ b
heq :
  Eq (α := obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj a) ⟶ obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj b))
    (Functor.map fiberInclusion ((Fiber.inducedFunctor ⋯).map f))
    (Functor.map fiberInclusion ((Fiber.inducedFunctor ⋯).map g))
⊢ f = g

Tactic:
simpa [cancel_mono, ← Cat.Hom.toNatIso_hom,
      ← Cat.Hom.toNatIso_inv] using ((Hom.ext_iff _ _).mp heq).2

Premises used: CategoryTheory.Cat.Hom.toNatIso_hom, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Cat.Hom.toNatIso_inv, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
h : Function.Surjective (Fiber.inducedFunctor ⋯).obj
⊢ (Fiber.inducedFunctor ⋯).EssSurj

Tactic:
apply essSurj_of_surj

Premises used: CategoryTheory.Functor.essSurj_of_surj
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ (obj fiberInclusion Y).base = S

Tactic:
simpa using Y.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ (obj fiberInclusion Y).base = S

Tactic:
have hYS : (fiberInclusion.obj Y).base = S := by simpa using Y.2
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
h :
  (Fiber.inducedFunctor ⋯).obj
      (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
        (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS) =
    Y
⊢ ∃ (a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)), (Fiber.inducedFunctor ⋯).obj a = Y

Tactic:
use hYS ▸ (fiberInclusion.obj Y).fiber
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
h :
  obj fiberInclusion
      ((Fiber.inducedFunctor ⋯).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS)) =
    obj fiberInclusion Y
⊢ (Fiber.inducedFunctor ⋯).obj
      (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
        (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS) =
    Y

Tactic:
apply fiberInclusion_obj_inj

Premises used: CategoryTheory.Functor.Fiber.fiberInclusion_obj_inj
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
h :
  (obj fiberInclusion
        ((Fiber.inducedFunctor ⋯).obj
          (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
            (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).base =
    (obj fiberInclusion Y).base
h₁ :
  (obj fiberInclusion
        ((Fiber.inducedFunctor ⋯).obj
          (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
            (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).fiber ≍
    (obj fiberInclusion Y).fiber
⊢ obj fiberInclusion
      ((Fiber.inducedFunctor ⋯).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS)) =
    obj fiberInclusion Y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
⊢ (obj fiberInclusion
        ((Fiber.inducedFunctor ⋯).obj
          (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
            (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).base =
    (obj fiberInclusion Y).base

Tactic:
simp [hYS]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
⊢ (obj fiberInclusion
        ((Fiber.inducedFunctor ⋯).obj
          (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
            (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).fiber ≍
    (obj fiberInclusion Y).fiber

Tactic:
simp [hYS]
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
⊢ IsEquivalence.{v₂, v₂, u₂, u₂} (C := p.Fiber S) (Fiber.inducedFunctor ⋯)

Tactic:
isEquivalence_of_iso (F := 𝟭 (Fiber p S)) (Iso.refl _)

Premises used: CategoryTheory.Functor.isEquivalence_of_iso, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
⊢ IsEquivalence.{v₂, v₂, u₂, u₂} (C := p.Fiber S) (Fiber.inducedFunctor ⋯)

Tactic:
exact isEquivalence_of_iso (F := 𝟭 (Fiber p S)) (Iso.refl _)

Premises used: CategoryTheory.Functor.isEquivalence_of_iso, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_2, u_1, v₂, u₂, v₁, u₁} p
S : 𝒮
⊢ Eq (α := CategoryTheory.Functor.{u_2, v₂, u_1, u₂} (Fib.{u_2, u_1, v₂, u₂, v₁, u₁} p S) 𝒳) (ι S)
    (inducedFunctor p S ⋙ fiberInclusion)

Tactic:
Fiber.inducedFunctor_comp (comp_const S)

Premises used: HasFibers.comp_const, CategoryTheory.Functor.comp, CategoryTheory.Functor.Fiber.inducedFunctor_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
⊢ IsEquivalence.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S) (inducedFunctor p S)

Tactic:
equiv S

Premises used: HasFibers.equiv, HasFibers.inducedFunctor