awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
h :
  ∀ (y : β),
    Eq (α := Bool)
      (ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true : ULift.{u, 0} Bool }))
          y))
      (ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false : ULift.{u, 0} Bool }))
          y))
⊢ Eq (α := β ⟶ ULift.{u, 0} Bool) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true })
    (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false })

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
y : β
⊢ Eq (α := Bool)
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true : ULift.{u, 0} Bool }))
        y))
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false : ULift.{u, 0} Bool }))
        y))

Tactic:
hsx.elim <| S.2 hf (↾fun _ => y)

Premises used: CategoryTheory.Sieve.downward_closed, TypeCat.ofHom, Not.elim
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
y : β
⊢ Eq (α := Bool)
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true : ULift.{u, 0} Bool }))
        y))
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false : ULift.{u, 0} Bool }))
        y))

Tactic:
exact hsx.elim <| S.2 hf (↾fun _ => y)

Premises used: CategoryTheory.Sieve.downward_closed, TypeCat.ofHom, Not.elim
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
⊢ Eq.{u + 1} (α := unop (op PUnit.{u + 1}) ⟶ ULift.{u, 0} Bool) (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := true })
    (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := false })

Tactic:
have : (↾fun _ => ULift.up true) = ↾fun _ => ULift.up false :=
    (hs PUnit (↾fun _ => x)).isSeparatedFor.ext
      fun β f hf => by
        dsimp
        ext y
        exact hsx.elim <| S.2 hf (↾fun _ => y)
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
this :
  Eq.{u + 1} (α := unop (op PUnit.{u + 1}) ⟶ ULift.{u, 0} Bool) (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := true })
    (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := false })
⊢ False

Tactic:
simp [ConcreteCategory.hom_ext_iff] at this

Premises used: CategoryTheory.ConcreteCategory.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.Faithful
⊢ (sheafCompose J F ⋙ sheafToPresheaf J B).Faithful

Tactic:
show (sheafToPresheaf _ _ ⋙ (whiskeringRight Cᵒᵖ A B).obj F).Faithful from inferInstance

Premises used: CategoryTheory.sheafCompose, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.ObjectProperty.lift, CategoryTheory.inducedFunctor, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.Faithful
inst_7 : F.Full
⊢ (sheafCompose J F ⋙ sheafToPresheaf J B).Full

Tactic:
show (sheafToPresheaf _ _ ⋙ (whiskeringRight Cᵒᵖ A B).obj F).Full from inferInstance

Premises used: CategoryTheory.sheafCompose, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.ObjectProperty.lift, CategoryTheory.inducedFunctor, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.Faithful
⊢ (sheafCompose J F).Faithful

Tactic:
Functor.Faithful.of_comp (sheafCompose J F) (sheafToPresheaf _ _)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.Functor.Faithful.of_comp, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.Full
inst_7 : F.Faithful
⊢ (sheafCompose J F).Full

Tactic:
Functor.Full.of_comp_faithful (sheafCompose J F) (sheafToPresheaf _ _)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.Functor.Full.of_comp_faithful, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf.{v₁, v₂, u₁, u₂} J A
f : G₁ ⟶ G₂
h : IsIso ((sheafCompose J F).map f)
rw :
  IsIso (X := obj (obj (whiskeringRight Cᵒᵖ A B) F) (obj (sheafToPresheaf J A) G₁))
    (map (obj (whiskeringRight Cᵒᵖ A B) F) (map (sheafToPresheaf J A) f))
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _),
      ← isIso_iff_of_reflects_iso _ ((whiskeringRight Cᵒᵖ A B).obj F)]

Premises used: Opposite, CategoryTheory.Functor.whiskeringRight, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.Functor.obj, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf.{v₁, v₂, u₁, u₂} J A
f : G₁ ⟶ G₂
h : IsIso ((sheafCompose J F).map f)
change :
  IsIso (X := obj (sheafToPresheaf J B) ((sheafCompose J F).obj G₁))
    (map (sheafToPresheaf J B) ((sheafCompose J F).map f))
⊢ IsIso (X := obj (obj (whiskeringRight Cᵒᵖ A B) F) (obj (sheafToPresheaf J A) G₁))
    (map (obj (whiskeringRight Cᵒᵖ A B) F) (map (sheafToPresheaf J A) f))

Tactic:
change IsIso ((sheafToPresheaf _ _).map ((sheafCompose J F).map f))

Premises used: CategoryTheory.sheafCompose, CategoryTheory.IsIso, CategoryTheory.Functor.map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf.{v₁, v₂, u₁, u₂} J A
f : G₁ ⟶ G₂
h : IsIso ((sheafCompose J F).map f)
⊢ IsIso (X := obj (sheafToPresheaf J B) ((sheafCompose J F).obj G₁))
    (map (sheafToPresheaf J B) ((sheafCompose J F).map f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_3 : J.HasSheafCompose F
⊢ sheafCompose_map J (𝟙 F) = 𝟙 (sheafCompose J F)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.sheafCompose_map, CategoryTheory.Functor.whiskerLeft, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
⊢ Eq (α := sheafCompose J F ⟶ sheafCompose J H) (sheafCompose_map J (η ≫ γ))
    (CategoryStruct.comp (Y := sheafCompose J G) (sheafCompose_map J η) (sheafCompose_map J γ))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, CategoryTheory.sheafCompose_map, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
rw :
  ∀ (hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) (X : C) (S : J.Cover X),
    Nonempty (IsLimit (S.multifork (P ⋙ F)))
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
rw [Presheaf.isSheaf_iff_multifork] at hP ⊢

Premises used: CategoryTheory.Presheaf.isSheaf_iff_multifork
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
obtain : ∀ (h : IsLimit (S.multifork P)), Nonempty (IsLimit (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
obtain ⟨h⟩ := hP X S
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
replace : ∀ (h : IsLimit (F.mapCone (S.multifork P))), Nonempty (IsLimit (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
replace h := isLimitOfPreserves F h
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit (F.mapCone (S.multifork P))
replace :
  ∀ (h : IsLimit ((Cone.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (S.multifork (P ⋙ F)))),
    Nonempty (IsLimit (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
replace h := Limits.IsLimit.ofIsoLimit h (S.mapMultifork F P)
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit ((Cone.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Nonempty.intro, CategoryTheory.GrothendieckTopology.Cover.multicospanComp, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit ((Cone.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
exact ⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
FA : A → A → Type u_1
CA : A → Type u_2
inst_2 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_2, v₂, u₂, u_1} A FA (CC := CA)
inst_4 : GrothendieckTopology.HasSheafCompose.{v₁, v₂, u_2, u₁, u₂, u_2 + 1} J (forget A (FC := FA) (CC := CA))
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x y : ToType.{u_2, v₂, u₂, u_1} (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op X))
h :
  ∀ (Y : C) (f : Y ⟶ X),
    S.arrows f →
      Eq (α := CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : CA (F.obj.obj (Opposite.op X))) → CA (F.obj.obj (Opposite.op Y)))
            x :
          CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : CA (F.obj.obj (Opposite.op X))) → CA (F.obj.obj (Opposite.op Y)))
            y :
          CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
⊢ x = y

Tactic:
(((isSheaf_iff_isSheaf_of_type _ _).1
    ((sheafCompose J (forget A)).obj F).2).isSeparated S hS).ext (fun _ _ hf => h _ _ hf)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.forget, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
FA : A → A → Type u_1
CA : A → Type u_2
inst_2 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_2, v₂, u₂, u_1} A FA (CC := CA)
inst_4 : GrothendieckTopology.HasSheafCompose.{v₁, v₂, u_2, u₁, u₂, u_2 + 1} J (forget A (FC := FA) (CC := CA))
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x y : ToType.{u_2, v₂, u₂, u_1} (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op X))
h :
  ∀ (Y : C) (f : Y ⟶ X),
    S.arrows f →
      Eq (α := CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : CA (F.obj.obj (Opposite.op X))) → CA (F.obj.obj (Opposite.op Y)))
            x :
          CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : CA (F.obj.obj (Opposite.op X))) → CA (F.obj.obj (Opposite.op Y)))
            y :
          CA (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y)))
⊢ x = y

Tactic:
exact (((isSheaf_iff_isSheaf_of_type _ _).1
    ((sheafCompose J (forget A)).obj F).2).isSeparated S hS).ext (fun _ _ hf => h _ _ hf)

Premises used: CategoryTheory.sheafCompose, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.forget, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
FA : A → A → Type u_1
CA : A → Type u_2
inst_2 : (X Y : A) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_2, v₂, u₂, u_1} A FA (CC := CA)
inst_4 : GrothendieckTopology.HasSheafCompose.{v₁, v₂, u_2, u₁, u₂, u_2 + 1} J (forget A (FC := FA) (CC := CA))
hF : IsSheaf J F
⊢ IsSeparated J F (FA := FA) (CA := CA)

Tactic:
Sheaf.isSeparated ⟨F, hF⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Sheaf.isSeparated
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Quiver.IsThin.{u₁, v₁} C
hC : Skeletal.{v₁, u₁} C
hF : F₁ ≅ F₂
⊢ F₁ = F₂

Tactic:
Functor.ext (fun X => hC ⟨hF.app X⟩) fun _ _ _ => Subsingleton.elim _ _

Premises used: CategoryTheory.Functor.ext, CategoryTheory.eqToHom, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.app, Subsingleton.elim, Eq.symm
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
hC : Skeletal.{v₁, u₁} C
⊢ Skeletal (Functor.{v₂, v₁, u₂, u₁} D C)

Tactic:
fun _ _ h =>
  h.elim (Functor.eq_of_iso hC)

Premises used: CategoryTheory.Functor.eq_of_iso, Nonempty.elim, CategoryTheory.Skeletal
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ Functor.Full.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (fromSkeleton C)

Tactic:
apply InducedCategory.full

Premises used: CategoryTheory.InducedCategory.full
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ Functor.Faithful.{v₁, v₁, u₁, u₁} (C := Skeleton.{v₁, u₁} C) (fromSkeleton C)

Tactic:
apply InducedCategory.faithful

Premises used: CategoryTheory.InducedCategory.faithful
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Skeleton.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
x : C
⊢ Eq.{v₁ + 1} (α := Quiver.Hom (V := Skeleton.{v₁, u₁} C) (toSkeleton x) (toSkeleton x))
    { hom := Iso.hom (fromSkeletonToSkeletonIso x) ≫ 𝟙 x ≫ Iso.inv (fromSkeletonToSkeletonIso x) } (𝟙 (toSkeleton x))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ { hom := Iso.hom (fromSkeletonToSkeletonIso X) ≫ (x ≫ x_1) ≫ Iso.inv (fromSkeletonToSkeletonIso Z) :
        InducedCategory.Hom (C := Quotient (isIsomorphicSetoid.{v₁, u₁} C)) (toSkeleton X) (toSkeleton Z) }.hom =
    InducedCategory.Hom.hom
      ({ hom := Iso.hom (fromSkeletonToSkeletonIso X) ≫ x ≫ Iso.inv (fromSkeletonToSkeletonIso Y) :
          InducedCategory.Hom (C := Quotient (isIsomorphicSetoid.{v₁, u₁} C)) (toSkeleton X) (toSkeleton Y) } ≫
        { hom := Iso.hom (fromSkeletonToSkeletonIso Y) ≫ x_1 ≫ Iso.inv (fromSkeletonToSkeletonIso Z) })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Skeleton.{v₁, u₁} C
h : X ≅ Y
⊢ Quotient.out X ≈ Quotient.out Y

Tactic:
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Skeleton.{v₁, u₁} C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y

Tactic:
simpa using Quotient.sound this

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Skeleton.{v₁, u₁} C
⊢ toSkeleton (Functor.obj (fromSkeleton C) X) = X

Tactic:
Quotient.out_eq _

Premises used: Quot.out, Quotient.out, CategoryTheory.InducedCategory, Classical.choose, Quotient.out_eq, CategoryTheory.Skeleton
-- Module: Mathlib.CategoryTheory.Skeletal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
⊢ Eq (α := Skeleton.{v₁, u₁} C) (toSkeleton X) (toSkeleton Y) ↔ Nonempty.{v₁ + 1} (X ≅ Y)

Tactic:
Quotient.eq

Premises used: CategoryTheory.IsIsomorphic, CategoryTheory.InducedCategory, Quotient.eq, CategoryTheory.Skeleton