awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
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) (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
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
⊢ Eq (α := (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F)))
        x :
      (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
    (NatTrans.app (J.toPlus (P ⋙ F)) x : (P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x)
have w : Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
  (CategoryStruct.comp (Y := F.obj ((J.plusObj P).obj x))
      (F.map
          (CategoryStruct.comp (Y :=
            multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
            (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop x)) (op ⊤))) :
        F.obj (P.obj x) ⟶ F.obj ((J.plusObj P).obj x))
      (NatTrans.app (Iso.hom (J.plusCompIso F P)) x : (J.plusObj P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x) :
    F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
  (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
    F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
Tactic: dsimp [toPlus]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
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) (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
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
⊢ Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y := F.obj ((J.plusObj P).obj x))
        (F.map
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P (unop x)) (op ⊤))) :
          F.obj (P.obj x) ⟶ F.obj ((J.plusObj P).obj x))
        (NatTrans.app (Iso.hom (J.plusCompIso F P)) x : (J.plusObj P ⋙ F).obj x ⟶ (J.plusObj (P ⋙ F)).obj x) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
have w : Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
  (CategoryStruct.comp (Y :=
      F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
      (F.map (Cover.toMultiequalizer ⊤ P) :
        F.obj (P.obj x) ⟶
          F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
      (CategoryStruct.comp (Y := obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
          (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
            obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
              obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
          (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤) :
            obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤) ⟶
              colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
        obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
          colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
    F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
  (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
      (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
    F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
Tactic: simp only [ι_plusCompIso_hom, Functor.map_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
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) (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
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x : Cᵒᵖ
⊢ Eq (α := F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y := obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
        (CategoryStruct.comp (Y :=
            F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
            (F.map (Cover.toMultiequalizer ⊤ P) :
              F.obj (P.obj x) ⟶
                F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
            (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
              obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
                obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
          F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
        (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤) :
          obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤) ⟶
            colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x))) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
        (Cover.toMultiequalizer ⊤ (P ⋙ F)) (colimit.ι (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
      F.obj (P.obj x) ⟶ (J.plusObj (P ⋙ F)).obj x)
have w : Eq (α := F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
  (CategoryStruct.comp (Y :=
      F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
      (F.map (Cover.toMultiequalizer ⊤ P) :
        F.obj (P.obj x) ⟶
          F.obj (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P)))
      (NatTrans.app (Iso.hom (J.diagramCompIso F P (unop x))) (op ⊤) :
        obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram P (unop x) ⋙ F) (op ⊤) ⟶
          obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤)) :
    F.obj (P.obj x) ⟶ obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram (P ⋙ F) (unop x)) (op ⊤))
  (Cover.toMultiequalizer ⊤ (P ⋙ F) :
    (P ⋙ F).obj (op (unop x)) ⟶
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ (P ⋙ F)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatiblePlus (goal)
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) (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
inst_6 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_7 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst_8 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ Eq (α := J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F) (Iso.inv (J.plusCompIso F P) : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F)
    (J.plusLift (whiskerRight (J.toPlus P) F) hP : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F)
have hγ : Eq (α := P ⋙ F ⟶ J.plusObj P ⋙ F)
  (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (J.toPlus (P ⋙ F) : P ⋙ F ⟶ J.plusObj (P ⋙ F))
      (Iso.inv (J.plusCompIso F P) : J.plusObj (P ⋙ F) ⟶ J.plusObj P ⋙ F) :
    P ⋙ F ⟶ J.plusObj P ⋙ F)
  (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
Tactic: apply J.plusLift_unique
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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_1 P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_9 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 :
  ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D),
    PreservesLimit (W.index P).multicospan F
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} D E ⥤ Functor.{v, v_2, u, u_2} Cᵒᵖ E)
    (obj (whiskeringLeft Cᵒᵖ D E) (J.sheafify P)) (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.sheafification E)
have refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} D E ⥤ Functor.{v, v_2, u, u_2} Cᵒᵖ E)
  (obj (whiskeringLeft Cᵒᵖ D E) (J.plusObj P) ⋙ J.plusFunctor E)
  ((obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.plusFunctor E) ⋙ J.plusFunctor E)
Tactic: refine J.plusFunctorWhiskerLeftIso _ ≪≫ ?_ ≪≫ associator _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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_1 P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
inst_9 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_10 :
  ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D),
    PreservesLimit (W.index P).multicospan F
⊢ Iso (C := Functor.{v_1, v_2, u_1, u_2} D E ⥤ Functor.{v, v_2, u, u_2} Cᵒᵖ E)
    (obj (whiskeringLeft Cᵒᵖ D E) (J.plusObj P) ⋙ J.plusFunctor E)
    ((obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.plusFunctor E) ⋙ J.plusFunctor E)
have refine : Iso (C := Functor.{v_1, v_2, u_1, u_2} D E ⥤ Functor.{v, v_2, u, u_2} Cᵒᵖ E)
  (obj (whiskeringLeft Cᵒᵖ D E) (J.plusObj P)) (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.plusFunctor E)
Tactic: refine isoWhiskerRight ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
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
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_7 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 :
  ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D),
    PreservesLimit (W.index P).multicospan F
⊢ Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ D E) (J.sheafify P)) F ⟶ obj (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.sheafification E) F)
    (NatTrans.app (Iso.hom (J.sheafificationWhiskerLeftIso P)) F :
      obj (obj (whiskeringLeft Cᵒᵖ D E) (J.sheafify P)) F ⟶ obj (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.sheafification E) F)
    (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F))
have dsimp : Eq (α := J.sheafify P ⋙ F ⟶ J.sheafify (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))
      (CategoryStruct.comp (Y := 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 (J.plusObj (P ⋙ F))) :
        J.plusObj (J.plusObj P ⋙ F) ⟶ J.sheafify (P ⋙ F)) :
    J.sheafify 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))
Tactic: dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
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
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_7 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst_8 :
  ∀ (F : Functor.{v_1, v_2, u_1, u_2} D E) (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D),
    PreservesLimit (W.index P).multicospan F
⊢ Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.sheafification E) F ⟶ obj (obj (whiskeringLeft Cᵒᵖ D E) (J.sheafify P)) F)
    (NatTrans.app (Iso.inv (J.sheafificationWhiskerLeftIso P)) F :
      obj (obj (whiskeringLeft Cᵒᵖ D E) P ⋙ J.sheafification E) F ⟶ obj (obj (whiskeringLeft Cᵒᵖ D E) (J.sheafify P)) F)
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
have dsimp : Eq (α := J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
  (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
      (𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (Iso.inv (J.plusCompIso F P)) :
        J.sheafify (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))
      (Iso.inv (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj P) ⋙ F) :
    J.sheafify (P ⋙ F) ⟶ J.sheafify 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) :
    J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
Tactic: dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
⊢ J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ≅ obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E
have refine : J.plusFunctor D ⋙ J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ≅
  obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E
Tactic: refine associator _ _ _ ≪≫ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
⊢ J.plusFunctor D ⋙ J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ≅
    obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E
have refine : J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E ≅
  obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E
Tactic: refine isoWhiskerLeft (J.plusFunctor D) (J.plusFunctorWhiskerRightIso _) ≪≫ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
⊢ J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E ≅
    obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E
have refine : J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E ≅
  (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E
Tactic: refine ?_ ≪≫ associator _ _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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
⊢ J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E ≅
    (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E
have refine : (J.plusFunctor D ⋙ obj (whiskeringRight Cᵒᵖ D E) F) ⋙ J.plusFunctor E ≅
  (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.plusFunctor E) ⋙ J.plusFunctor E
Tactic: refine (associator _ _ _).symm ≪≫ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CompatibleSheafification (goal)
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 (α :=
    (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P ⟶
      (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P)
    (NatTrans.app (Iso.hom (J.sheafificationWhiskerRightIso F)) P :
      (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P ⟶
        (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P)
    (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F))
have dsimp : 𝟙 (J.plusObj (J.plusObj P) ⋙ F) ≫
    Iso.hom (J.plusCompIso F (J.plusObj P)) ≫
      CategoryStruct.comp (Y := 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 (J.plusObj (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)))
Tactic: dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]