awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD ((J.diagram P X).obj (op S))) → CD ((J.plusObj P).obj (op X)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
              (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                      (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
                  (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                x :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD ((J.diagram P X).obj (op S))) :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))
have h : Eq (α := CD ((J.diagram P X).obj (op S)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
        (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) sorry) :
            (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
          x :
        CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
    CD ((J.diagram P X).obj (op S)))
  ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
      (Meq.mk (FD := FD) (CD := CD) S x) :
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ Eq (α := CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
          (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                  (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
              (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
            x :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD ((J.diagram P X).obj (op S)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
        (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))
have h : Eq (α := CD (multiequalizer (S.index P)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Multiequalizer.lift (S.index P)
            (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
            (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) sorry) :
        (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) sorry) :
            (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
          x :
        CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
    CD (multiequalizer (S.index P)))
  ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
      (Meq.mk (FD := FD) (CD := CD) S x) :
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))
Tactic: dsimp [diagram]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
⊢ Eq (α := CD ((S.index P).left i))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
          (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left i))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (S.index P)
                  (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
                  (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) ⋯) :
              (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                      (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) ⋯) :
                  (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                x :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD (multiequalizer (S.index P))) :
      CD ((S.index P).left i))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
          (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left i))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD ((S.index P).left i))
have h : (ConcreteCategory.hom (FC := FD) (CC := CD) (P.map (Cover.Arrow.map i e).f.op) :
      (a : CD (P.obj (op X))) → CD ((S.index P).left i))
    x =
  (↑(Meq.mk (FD := FD) (CD := CD) S x) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
Tactic: simp only [← ConcreteCategory.comp_apply, Category.assoc, Multiequalizer.lift_ι,
    Meq.equiv_symm_eq_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
⊢ Eq (α := CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op I.Y)) :
          (a : CD (P.obj (op I.Y))) → CD ((J.plusObj P).obj (op I.Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
      CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD ((J.plusObj P).obj (op I.Y)))
have dsimp : Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (CategoryStruct.comp (Y :=
            multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
            (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P I.Y) (op ⊤))) :
        (a : CD (P.obj (op I.Y))) → CD (colimit (J.diagram P I.Y)))
      ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
    CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (CategoryStruct.comp (Y := colimit ((J.pullback I.f.op.unop).op ⋙ J.diagram P I.Y))
            (colimMap (J.diagramPullback P I.f.op.unop)) (colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op)) :
        (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P I.Y)))
      (mk (FD := FD) (CD := CD) x) :
    CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
Tactic: dsimp only [toPlus, plusObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
⊢ Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P I.Y) (op ⊤))) :
          (a : CD (P.obj (op I.Y))) → CD (colimit (J.diagram P I.Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y := colimit ((J.pullback I.f.op.unop).op ⋙ J.diagram P I.Y))
              (colimMap (J.diagramPullback P I.f.op.unop))
              (colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op)) :
          (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P I.Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
have delta : Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (CategoryStruct.comp (Y :=
            multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
            (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op I.Y))
              (fun (I_1 : (Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤).L) ↦ P.map I_1.f.op) sorry)
            (colimit.ι (J.diagram P I.Y) (op ⊤))) :
        (a : CD (P.obj (op I.Y))) → CD (colimit (J.diagram P I.Y)))
      ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
    CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (CategoryStruct.comp (Y := colimit ((J.pullback I.f.op.unop).op ⋙ J.diagram P I.Y))
            (colimMap (J.diagramPullback P I.f.op.unop)) (colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op)) :
        (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P I.Y)))
      (mk (FD := FD) (CD := CD) x) :
    CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
Tactic: delta Cover.toMultiequalizer
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ Eq (α := CD (P.obj (op i.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map (Cover.Arrow.map i e).f.op) :
          (a : CD (P.obj (op I.Y))) → CD (P.obj (op i.Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
      CD (P.obj (op i.Y)))
    (((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _
              (Multiequalizer.ι (S.index P) (Cover.Arrow.base i)) :
            FD (multiequalizer (S.index P)) (P.obj (op i.Y))) :
          (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (P.obj (op i.Y)))
have h : (ConcreteCategory.hom (FC := FD) (CC := CD) (P.map (Cover.Arrow.map i e).f.op) :
      (a : CD (P.obj (op I.Y))) → CD (P.obj (op i.Y)))
    ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) =
  (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) (Cover.Arrow.base i)
Tactic: rw [dsimp% Meq.equiv_symm_eq_apply x i.base]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
⊢ ∃ (S : J.Cover X) (y : Meq (FD := FD) (CD := CD) P S), x = mk (FD := FD) (CD := CD) y
have obtain : ∀ (S : (J.Cover X)ᵒᵖ) (y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.diagram P X).obj S))
  (h :
    (ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
          (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
        y =
      x),
  ∃ (S : J.Cover X) (y : Meq (FD := FD) (CD := CD) P S), x = mk (FD := FD) (CD := CD) y
Tactic: obtain ⟨S, y, h⟩ := Concrete.colimit_exists_rep (J.diagram P X) x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.diagram P X).obj S)
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
      y =
    x
⊢ ∃ (S : J.Cover X) (y : Meq (FD := FD) (CD := CD) P S), x = mk (FD := FD) (CD := CD) y
have h₁ : x =
  mk (FD := FD) (CD := CD) (S := unop S)
    ((Meq.equiv (FD := FD) (CD := CD) P (unop S) : (a : ToType (multiequalizer ((unop S).index P))) → Meq P (unop S)) y)
Tactic: use S.unop, Meq.equiv _ _ y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.diagram P X).obj S)
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
      y =
    x
⊢ x =
    mk (FD := FD) (CD := CD) (S := unop S)
      ((Meq.equiv (FD := FD) (CD := CD) P (unop S) : (a : ToType (multiequalizer ((unop S).index P))) → Meq P (unop S))
        y)
have h₁ : Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
      y :
    CD (colimit (J.diagram P X)))
  (mk (FD := FD) (CD := CD) (S := unop S)
      ((Meq.equiv (FD := FD) (CD := CD) P (unop S) : (a : ToType (multiequalizer ((unop S).index P))) → Meq P (unop S))
        y) :
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.diagram P X).obj S)
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
      y =
    x
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
          (a : CD ((J.diagram P X).obj S)) → CD (colimit (J.diagram P X)))
        y :
      CD (colimit (J.diagram P X)))
    (mk (FD := FD) (CD := CD) (S := unop S)
        ((Meq.equiv (FD := FD) (CD := CD) P (unop S) :
            (a : ToType (multiequalizer ((unop S).index P))) → Meq P (unop S))
          y) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
have h₁ : Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD (multiequalizer ((unop S).index P))) → CD (colimit (J.diagram P X)))
      y :
    CD (colimit (J.diagram P X)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) S) :
        (a : CD (multiequalizer ((unop S).index P))) → CD (colimit (J.diagram P X)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (unop S)) :
            (a : Meq P (unop S)) → ToType (multiequalizer ((unop S).index P)))
          ((Meq.equiv (FD := FD) (CD := CD) P (unop S) :
              (a : ToType (multiequalizer ((unop S).index P))) → Meq P (unop S))
            y) :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer ((unop S).index P))) :
    CD (colimit (J.diagram P X)))
Tactic: dsimp [mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := 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 S
y : Meq (FD := FD) (CD := CD) P T
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
      (mk (FD := FD) (CD := CD) y) ↔
    ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
have mp : Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y) →
  ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
Tactic: constructor