-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- An object is initial if and only if its fiber is empty. -/
lemma initial_iff_fiber_empty (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (F.obj X)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this : PreservesFiniteColimits (forget FintypeCat)
⊢ ReflectsColimit (empty FintypeCat) (forget FintypeCat)

Tactic:
show ReflectsColimit (Functor.empty.{0} _) FintypeCat.incl

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this : PreservesFiniteColimits (forget FintypeCat)
⊢ ReflectsColimit (empty FintypeCat) FintypeCat.incl

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ PreservesFiniteColimits FintypeCat.incl

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this : PreservesFiniteColimits (forget FintypeCat)
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier

Tactic:
haveI : ReflectsColimit (Functor.empty.{0} _) (forget FintypeCat) := by
  show ReflectsColimit (Functor.empty.{0} _) FintypeCat.incl
  infer_instance

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this✝ : PreservesFiniteColimits (forget FintypeCat)
this : ReflectsColimit (empty FintypeCat) (forget FintypeCat)
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this : PreservesFiniteColimits (forget FintypeCat)
⊢ ReflectsColimit (empty FintypeCat) FintypeCat.incl

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ PreservesFiniteColimits (forget FintypeCat)

Tactic:
show PreservesFiniteColimits FintypeCat.incl

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ PreservesFiniteColimits FintypeCat.incl

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier

Tactic:
haveI : PreservesFiniteColimits (forget FintypeCat) := by
  show PreservesFiniteColimits FintypeCat.incl
  infer_instance

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this : PreservesFiniteColimits (forget FintypeCat)
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
this✝ : PreservesFiniteColimits (forget FintypeCat)
this : ReflectsColimit (empty FintypeCat) (forget FintypeCat)
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier

Tactic:
exact Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (F.obj X).carrier

Tactic:
rw [(IsInitial.isInitialIffObj F X).nonempty_congr]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).carrier