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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| F.map
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) W)
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (colimMap (J.diagramPullback P f.unop)) (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))
have a : (F.map
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) W)
      (colimit.desc (J.diagram P (unop X))
          (obj (Cocone.precompose (J.diagramPullback P f.unop))
            (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))) ≫
        colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
  F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
Tactic: dsimp [colimMap, IsColimit.map, colimit.pre]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| (F.map
      (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
        (colimit.ι (J.diagram P (unop X)) W)
        (colimit.desc (J.diagram P (unop X))
            (obj (Cocone.precompose (J.diagramPullback P f.unop))
              (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))) ≫
          colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
            (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
have a : (F.map
    ((obj (Cocone.precompose (J.diagramPullback P f.unop))
              (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))).ι.app
        W ≫
      colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
        (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) :
  F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
Tactic: simp only [colimit.ι_desc_assoc, colimit.ι_desc]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| (F.map
      ((obj (Cocone.precompose (J.diagramPullback P f.unop))
                (colimit.cocone ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))).ι.app
          W ≫
        colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
have a : (F.map
    (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
          (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry ≫
        colimit.ι ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)) W)
      (colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
        (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
  F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
Tactic: dsimp [Cocone.precompose]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| (F.map
      (CategoryStruct.comp (Y := colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)))
        (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
            (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯ ≫
          colimit.ι ((J.pullback f.unop).op ⋙ J.diagram P (unop Y)) W)
        (colimit.desc ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))
          (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y)))))) :
    F.obj (multiequalizer ((unop W).index P)) ⟶ F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
have a : F.map
  (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
    (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
      (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry)
    (NatTrans.app (Cocone.ι (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) W))
Tactic: simp only [Category.assoc, colimit.ι_desc]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (NatTrans.app (Cocone.ι (Cocone.whisker (J.pullback f.unop).op (colimit.cocone (J.diagram P (unop Y))))) W))
have a : F.map
  (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
    (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
      (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry)
    (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
Tactic: dsimp [Cocone.whisker]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| F.map
    (CategoryStruct.comp (Y := multiequalizer (((unop W).pullback f.unop).index P))
      (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
        (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯)
      (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
have a : CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
  (F.map
    (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
      (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry))
  (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
Tactic: rw [F.map_comp]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X))))
    (F.map (colimit.ι (J.diagram P (unop X)) W))
    (CategoryStruct.comp (Y := F.obj (colimit ((J.pullback f.unop).op ⋙ J.diagram P (unop Y))))
      (F.map (colimMap (J.diagramPullback P f.unop)))
      (F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op)))
have a : CategoryStruct.comp (Y := F.obj (multiequalizer (((unop W).pullback f.unop).index P)))
  (F.map
    (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
      (fun (I : ((unop W).pullback f.unop).Arrow) ↦ Multiequalizer.ι ((unop W).index P) I.base) sorry))
  (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
Tactic: simp only [← F.map_comp]
        dsimp [colimMap, IsColimit.map, colimit.pre]
        simp only [colimit.ι_desc_assoc, colimit.ι_desc]
        dsimp [Cocone.precompose]
        simp only [Category.assoc, colimit.ι_desc]
        dsimp [Cocone.whisker]
        rw [F.map_comp]
-- 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 Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
| (CategoryStruct.comp (Y := F.obj (colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y))))
      (F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop))))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y))))
          (colimit.isColimit (J.diagram P (unop Y) ⋙ F)))) :
    F.obj (multiequalizer (((unop W).pullback f.unop).index P)) ⟶
      colimit (J := (J.Cover (unop Y))ᵒᵖ) (J.diagram P (unop Y) ⋙ F))
have a : NatTrans.app (Cocone.ι (colimit.cocone (J.diagram P (unop Y) ⋙ F))) (op ((unop W).pullback f.unop))
Tactic: erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P Y.unop))).fac]
-- 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
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
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
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
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
⊢ Eq (α := J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))
    ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))
    (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
        (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)) :
      J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ G))
have w : ∀ (X : Cᵒᵖ),
  Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
Tactic: ext X
-- 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
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
F G : Functor.{v_1, v_2, u_1, u_2} D E
η : F ⟶ G
P : Functor.{v, v_1, u, u_1} Cᵒᵖ D
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
inst_9 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst_10 : ∀ (X : C) (W : J.Cover X) (P : Functor.{v, v_1, u, u_1} Cᵒᵖ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
⊢ Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (P ⋙ G)).obj X)
have w : ∀ (j : (J.Cover (unop X))ᵒᵖ),
  Eq (α := obj (J.diagram P (unop X) ⋙ F) j ⟶ (J.plusObj (P ⋙ G)).obj X)
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (J.Cover (unop X))ᵒᵖ)
          (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
            (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
        j)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
      (NatTrans.app ((J.plusObj P).whiskerLeft η ≫ Iso.hom (J.plusCompIso G P)) X))
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (J.Cover (unop X))ᵒᵖ)
          (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
            (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
        j)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
      (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (P.whiskerLeft η) : J.plusObj (P ⋙ F) ⟶ J.plusObj (P ⋙ G)))
        X))
Tactic: apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
-- 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
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
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ F))
    (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q) : J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ 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 η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)) :
      J.plusObj P ⋙ F ⟶ J.plusObj (Q ⋙ F))
have w : ∀ (X : Cᵒᵖ),
  Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
Tactic: ext X
-- 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
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
P Q : Functor.{v, v_1, u, u_1} Cᵒᵖ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ Eq (α := (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
        X :
      (J.plusObj P ⋙ F).obj X ⟶ (J.plusObj (Q ⋙ F)).obj X)
have w : ∀ (j : (J.Cover (unop X))ᵒᵖ),
  Eq (α := obj (J.diagram P (unop X) ⋙ F) j ⟶ (J.plusObj (Q ⋙ F)).obj X)
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (J.Cover (unop X))ᵒᵖ)
          (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
            (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
        j)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
      (NatTrans.app (whiskerRight (J.plusMap η) F ≫ Iso.hom (J.plusCompIso F Q)) X))
    (CategoryStruct.comp (Y :=
      obj
        (obj (const (J.Cover (unop X))ᵒᵖ)
          (Cocone.pt (J := (J.Cover (unop X))ᵒᵖ) (F := J.diagram P (unop X) ⋙ F)
            (F.mapCocone (colimit.cocone (J.diagram P (unop X))))))
        j)
      (NatTrans.app (Cocone.ι (F.mapCocone (colimit.cocone (J.diagram P (unop X))))) j)
      (NatTrans.app
        (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
          (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (J.plusMap (whiskerRight η F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (Q ⋙ F)))
        X))
Tactic: apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
-- 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
⊢ Eq (α := P ⋙ F ⟶ J.plusObj (P ⋙ F))
    (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)) :
      P ⋙ F ⟶ J.plusObj (P ⋙ F))
    (J.toPlus (P ⋙ F) : P ⋙ F ⟶ J.plusObj (P ⋙ F))
have w : ∀ (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)
Tactic: ext