awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := P.obj X ⟶ Functor.obj (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤)))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
      (P.map f ≫
        Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (Functor.map (J.diagram P (unop Y)) e.op))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
        (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
        (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) ⋯))
have e_a : ∀ (I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L),
  CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback f.unop).obj ⊤))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (P.map f ≫
          Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
            (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
        (Functor.map (J.diagram P (unop Y)) e.op))
      (Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I) =
    CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback f.unop).obj ⊤))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
        (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
          (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
          (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) sorry))
      (Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I)
Tactic: refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L
⊢ CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback f.unop).obj ⊤))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
        (P.map f ≫
          Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
            (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (Functor.map (J.diagram P (unop Y)) e.op))
      (Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I) =
    CategoryStruct.comp (Y := multiequalizer ((unop (op ((J.pullback f.unop).obj ⊤))).index P))
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
          (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
          (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) ⋯))
      (Multiequalizer.ι ((unop (op ((J.pullback f.unop).obj ⊤))).index P) I)
have e_a : P.map f ≫
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop Y)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop Y) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
      (CategoryStruct.comp (Y := multiequalizer (((J.pullback f.unop).obj ⊤).index P))
        (Functor.map (J.diagram P (unop Y)) e.op) (Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I)) =
  CategoryStruct.comp (Y :=
    multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ P))
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop X)))
      (fun (I : (Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
    (CategoryStruct.comp (Y := multiequalizer (((J.pullback f.unop).obj ⊤).index P))
      (Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P)
        (Functor.obj (C := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)) (op ⊤))
        (fun (I : ((J.pullback f.unop).obj ⊤).shape.L) ↦ Multiequalizer.ι (Cover.index ⊤ P) (Cover.Arrow.base I)) sorry)
      (Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I))
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
⊢ Eq (α := P ⟶ J.plusObj Q) (η ≫ J.toPlus Q) (J.toPlus P ≫ J.plusMap η)
have w : ∀ (x : Cᵒᵖ),
  Eq (α := P.obj x ⟶ (J.plusObj Q).obj x) (NatTrans.app (η ≫ J.toPlus Q) x) (NatTrans.app (J.toPlus P ≫ J.plusMap η) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
x : Cᵒᵖ
⊢ Eq (α := P.obj x ⟶ (J.plusObj Q).obj x) (NatTrans.app (η ≫ J.toPlus Q) x) (NatTrans.app (J.toPlus P ≫ J.plusMap η) x)
have w : Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
  (η.app x ≫
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
      (Cover.toMultiequalizer ⊤ Q) (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
  (CategoryStruct.comp (Y := (J.plusObj P).obj x)
    (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 ⊤)))
    (colimMap (J.diagramNatTrans η (unop x))))
Tactic: dsimp [toPlus, plusMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
x : Cᵒᵖ
⊢ Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
    (η.app x ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
        (Cover.toMultiequalizer ⊤ Q) (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
    (CategoryStruct.comp (Y := (J.plusObj P).obj x)
      (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 ⊤)))
      (colimMap (J.diagramNatTrans η (unop x))))
have w : Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
  (η.app x ≫
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
      (Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) sorry)
      (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
  (CategoryStruct.comp (Y := (J.plusObj P).obj x)
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
      (colimit.ι (J.diagram P (unop x)) (op ⊤)))
    (colimMap (J.diagramNatTrans η (unop x))))
Tactic: delta Cover.toMultiequalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
x : Cᵒᵖ
⊢ Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
    (η.app x ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
        (Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) ⋯)
        (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
    (CategoryStruct.comp (Y := (J.plusObj P).obj x)
      (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
        (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
        (colimit.ι (J.diagram P (unop x)) (op ⊤)))
      (colimMap (J.diagramNatTrans η (unop x))))
have w : Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
  (η.app x ≫
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
      (Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) sorry)
      (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
  (CategoryStruct.comp (Y :=
    multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
      (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) sorry)
    (NatTrans.app (J.diagramNatTrans η (unop x)) (op ⊤) ≫ colimit.ι (J.diagram Q (unop x)) (op ⊤)))
Tactic: simp only [ι_colimMap, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
x : Cᵒᵖ
⊢ Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
    (η.app x ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
        (Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) ⋯)
        (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ P))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯)
      (NatTrans.app (J.diagramNatTrans η (unop x)) (op ⊤) ≫ colimit.ι (J.diagram Q (unop x)) (op ⊤)))
have w : Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
  (CategoryStruct.comp (Y :=
    multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
    (η.app x ≫
      Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) sorry)
    (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
  (CategoryStruct.comp (Y := Functor.obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram Q (unop x)) (op ⊤))
    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) sorry ≫
      NatTrans.app (J.diagramNatTrans η (unop x)) (op ⊤))
    (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
Tactic: simp_rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
x : Cᵒᵖ
⊢ Eq (α := P.obj x ⟶ (J.plusObj Q).obj x)
    (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
      (η.app x ≫
        Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) ⋯)
      (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
    (CategoryStruct.comp (Y := Functor.obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram Q (unop x)) (op ⊤))
      (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
          (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯ ≫
        NatTrans.app (J.diagramNatTrans η (unop x)) (op ⊤))
      (colimit.ι (J.diagram Q (unop x)) (op ⊤)))
have w : Eq (α := P.obj x ⟶ multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
  (η.app x ≫
      Multiequalizer.lift (Cover.index ⊤ Q) (Q.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ Q.map I.f.op) sorry :
    P.obj x ⟶ multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤) (Cover.index ⊤ Q))
  (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op (unop x)))
        (fun (I : (Cover.shape.{v, u} (C := C) (X := unop x) (J := J) ⊤).L) ↦ P.map I.f.op) sorry ≫
      NatTrans.app (J.diagramNatTrans η (unop x)) (op ⊤) :
    P.obj x ⟶ Functor.obj (C := (J.Cover (unop x))ᵒᵖ) (J.diagram Q (unop x)) (op ⊤))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
⊢ J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)
have w : ∀ (X : Cᵒᵖ), NatTrans.app (J.plusMap (J.toPlus P)) X = NatTrans.app (J.toPlus (J.plusObj P)) X
Tactic: ext X : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
⊢ NatTrans.app (J.plusMap (J.toPlus P)) X = NatTrans.app (J.toPlus (J.plusObj P)) X
have w : ∀ (S : (J.Cover (unop X))ᵒᵖ),
  Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.plusMap (J.toPlus P)) X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.toPlus (J.plusObj P)) X)
Tactic: refine colimit.hom_ext (fun S => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.plusMap (J.toPlus P)) X)
    (colimit.ι (J.diagram P (unop X)) S ≫ NatTrans.app (J.toPlus (J.plusObj P)) X)
have w : Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
  (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
    (colimit.ι (J.diagram P (unop X)) S)
    (colimMap
      (J.diagramNatTrans
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := sorry }
        (unop X))))
  (colimit.ι (J.diagram P (unop X)) S ≫
    CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
      (Cover.toMultiequalizer ⊤ (J.plusObj P)) (colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)))
Tactic: dsimp only [plusMap, toPlus]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop X))ᵒᵖ) (J.diagram P (unop X)))
      (colimit.ι (J.diagram P (unop X)) S)
      (colimMap
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))))
    (colimit.ι (J.diagram P (unop X)) S ≫
      CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (Cover.toMultiequalizer ⊤ (J.plusObj P)) (colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)))
have w : Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
  (NatTrans.app
      (J.diagramNatTrans
        {
          app := fun (X : Cᵒᵖ) ↦
            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 ⊤)),
          naturality := sorry }
        (unop X))
      S ≫
    colimit.ι (J.diagram (J.plusObj P) (unop X)) S)
  (CategoryStruct.comp (Y :=
      multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
      (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
      (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op) ≫
    colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S)))
Tactic: rw [ι_colimMap, ← colimit.w _ e.op, ← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ (J.plusObj (J.plusObj P)).obj X)
    (NatTrans.app
        (J.diagramNatTrans
          {
            app := fun (X : Cᵒᵖ) ↦
              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 ⊤)),
            naturality := ⋯ }
          (unop X))
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S)
    (CategoryStruct.comp (Y :=
        multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
        (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
        (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S)))
have w : Eq (α := Functor.obj (J.diagram P (unop X)) S ⟶ Functor.obj (J.diagram (J.plusObj P) (unop X)) S)
  (NatTrans.app
    (J.diagramNatTrans
      {
        app := fun (X : Cᵒᵖ) ↦
          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 ⊤)),
        naturality := sorry }
      (unop X))
    S)
  (CategoryStruct.comp (Y :=
    multiequalizer (J := Cover.shape.{v, u} (C := C) (X := unop X) (J := J) ⊤) (Cover.index ⊤ (J.plusObj P)))
    (colimit.ι (J.diagram P (unop X)) S ≫ Cover.toMultiequalizer ⊤ (J.plusObj P))
    (Functor.map (J.diagram (J.plusObj P) (unop X)) e.op))
Tactic: congr 1