awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
dsimp :
  CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
      ((𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫
            CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
              (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
              (𝟙 (J.plusObj (J.plusObj P ⋙ F)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))) ≫
          Iso.inv (J.plusCompIso F (J.plusObj P)) :
        J.sheafify (P ⋙ F) ⟶ J.plusObj (J.plusObj P) ⋙ F)
      (𝟙 (J.plusObj (J.plusObj P) ⋙ F) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F) =
    CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
      (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
      (Iso.inv (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.sheafify P ⋙ F)
⊢ Eq (α :=
    (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P ⟶
      (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P)
    (NatTrans.app (Iso.inv (J.sheafificationWhiskerRightIso F)) P :
      (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P ⟶
        (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P)
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)

Tactic:
dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]

Premises used: CategoryTheory.GrothendieckTopology.sheafifyCompIso, CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
⊢ CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
      ((𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫
            CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
              (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
              (𝟙 (J.plusObj (J.plusObj P ⋙ F)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))) ≫
          Iso.inv (J.plusCompIso F (J.plusObj P)) :
        J.sheafify (P ⋙ F) ⟶ J.plusObj (J.plusObj P) ⋙ F)
      (𝟙 (J.plusObj (J.plusObj P) ⋙ F) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F) =
    CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
      (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
      (Iso.inv (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.sheafify P ⋙ F)

Tactic:
simp only [sheafify, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.GrothendieckTopology.sheafify, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
simp :
  Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
            (whiskerRight (J.plusMap (J.toPlus P)) F : J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F)
            (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
                (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
                (J.plusMap (Iso.hom (J.plusCompIso F P)) :
                  J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
              J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
⊢ Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.sheafify P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))

Tactic:
simp only [toSheafify, sheafify, whiskerRight_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.toSheafify, CategoryTheory.GrothendieckTopology.sheafify, CategoryTheory.Functor.whiskerRight_comp
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
a :
  (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
      (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
    J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
| (whiskerRight (J.plusMap (J.toPlus P)) F ≫ Iso.hom (J.plusCompIso F (J.plusObj P)) :
    J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))

Tactic:
rw [plusCompIso_whiskerRight]

Premises used: CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
slice_lhs :
  Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
                (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
                (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
              J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
⊢ Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
            (whiskerRight (J.plusMap (J.toPlus P)) F : J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F)
            (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
                (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
                (J.plusMap (Iso.hom (J.plusCompIso F P)) :
                  J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
              J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))

Tactic:
slice_lhs 2 3 => rw [plusCompIso_whiskerRight]

Premises used: CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
rw :
  Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))
⊢ Eq (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
        (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
      P ⋙ F ⟶ J.sheafify P ⋙ F)
    (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)

Tactic:
rw [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
⊢ Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
FD : D → D → Type u_3
CD : D → Type u_4
inst_9 : (X Y : D) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : ConcreteCategory.{u_4, v_1, u_1, u_3} D FD (CC := CD)
inst_11 : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_13 : ReflectsIsomorphisms.{v_1, u_1, u_4, u_4 + 1} (forget D (FC := FD) (CC := CD))
a :
  Eq (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
        (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
      P ⋙ F ⟶ J.sheafify P ⋙ F)
    (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
⊢ Eq (α := J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
    (J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯ : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)

Tactic:
apply J.sheafifyLift_unique

Premises used: CategoryTheory.GrothendieckTopology.sheafifyLift_unique
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
FD : D → D → Type u_3
CD : D → Type u_4
inst_9 : (X Y : D) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : ConcreteCategory.{u_4, v_1, u_1, u_3} D FD (CC := CD)
inst_11 : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_13 : ReflectsIsomorphisms.{v_1, u_1, u_4, u_4 + 1} (forget D (FC := FD) (CC := CD))
a :
  Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))
⊢ Eq (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
        (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
      P ⋙ F ⟶ J.sheafify P ⋙ F)
    (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)

Tactic:
rw [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_3 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst_4 : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_7 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
FD : D → D → Type u_3
CD : D → Type u_4
inst_9 : (X Y : D) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : ConcreteCategory.{u_4, v_1, u_1, u_3} D FD (CC := CD)
inst_11 : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_13 : ReflectsIsomorphisms.{v_1, u_1, u_4, u_4 + 1} (forget D (FC := FD) (CC := CD))
⊢ Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S : Sieve X).arrows f
⊢ (↑S : Sieve X).arrows g

Tactic:
simpa only [← h] using hf
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S : Sieve X).arrows f
subst :
  (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow } =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := ⋯ }
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow } =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := g, hf := ⋯ }

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
Y : C
f : Y ⟶ X
hf : (↑S : Sieve X).arrows f
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow } =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := ⋯ }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x y : Meq (FD := FD) (CD := CD) P S
h : ∀ (I : S.Arrow), (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I = (↑y : (I : S.Arrow) → ToType (P.obj (op I.Y))) I
⊢ x = y

Tactic:
Subtype.ext <| funext <| h

Premises used: CategoryTheory.Meq, funext, Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
I : S.Relation
⊢ Eq (α := CD (P.obj (op I.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.r.g₁.op) :
          (a : CD (P.obj (op I.fst.Y))) → CD (P.obj (op I.r.Z)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) (S.shape.fst I)) :
      CD (P.obj (op I.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.r.g₂.op) :
          (a : CD (P.obj (op I.snd.Y))) → CD (P.obj (op I.r.Z)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) (S.shape.snd I)) :
      CD (P.obj (op I.r.Z)))

Tactic:
x.2 _

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S T : J.Cover X
x : Meq (FD := FD) (CD := CD) P T
e : S ⟶ T
I : S.Arrow
⊢ (↑(x.refine (FD := FD) (CD := CD) e) : (I : S.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑x : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := I.Y, f := I.f, hf := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
Y X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
f : Y ⟶ X
I : ((J.pullback f).obj S).Arrow
⊢ (↑(x.pullback (FD := FD) (CD := CD) f) : (I : ((J.pullback f).obj S).Arrow) → ToType (P.obj (op I.Y))) I =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := I.Y, f := I.f ≫ f, hf := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
Y X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S T : J.Cover X
h : S ⟶ T
f : Y ⟶ X
x : Meq (FD := FD) (CD := CD) P T
⊢ (x.pullback (FD := FD) (CD := CD) f).refine (FD := FD) (CD := CD) ((J.pullback f).map h) =
    (x.refine (FD := FD) (CD := CD) h).pullback (FD := FD) (CD := CD) f

Tactic:
rfl

Premises used: CategoryTheory.Meq.pullback, CategoryTheory.Meq.refine, rfl