awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α :=
    (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P ⟶
      (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P)
    (NatTrans.app (Iso.inv (J.sheafificationWhiskerRightIso F)) P :
      (obj (whiskeringRight Cᵒᵖ D E) F ⋙ J.sheafification E).obj P ⟶
        (J.sheafification D ⋙ obj (whiskeringRight Cᵒᵖ D E) F).obj P)
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
have dsimp : CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
    ((𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫
          CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
            (𝟙 (J.plusObj (J.plusObj P ⋙ F)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))) ≫
        Iso.inv (J.plusCompIso F (J.plusObj P)) :
      J.sheafify (P ⋙ F) ⟶ J.plusObj (J.plusObj P) ⋙ F)
    (𝟙 (J.plusObj (J.plusObj P) ⋙ F) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F) =
  CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
    (J.plusMap (Iso.inv (J.plusCompIso F P)) : J.plusObj (J.plusObj (P ⋙ F)) ⟶ J.plusObj (J.plusObj P ⋙ F))
    (Iso.inv (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.sheafify P ⋙ F)
Tactic: dsimp [sheafificationWhiskerRightIso, 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
⊢ Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.sheafify P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
      P ⋙ F ⟶ J.sheafify (P ⋙ F))
    (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
have simp : Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
      (CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
          (whiskerRight (J.plusMap (J.toPlus P)) F : J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F)
          (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
              (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
              (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
            J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
        J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
    P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
Tactic: simp only [toSheafify, sheafify, whiskerRight_comp, Category.assoc]
-- 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
| (whiskerRight (J.plusMap (J.toPlus P)) F ≫ Iso.hom (J.plusCompIso F (J.plusObj P)) :
    J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
have a : (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
    (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
  J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
Tactic: rw [plusCompIso_whiskerRight]
-- 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 (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P) ⋙ F)
            (whiskerRight (J.plusMap (J.toPlus P)) F : J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P) ⋙ F)
            (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
                (Iso.hom (J.plusCompIso F (J.plusObj P)) : J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
                (J.plusMap (Iso.hom (J.plusCompIso F P)) :
                  J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
              J.plusObj (J.plusObj P) ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
have slice_lhs : Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
      (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
          (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
              (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
              (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
            J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
          (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
        J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
    P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
Tactic: slice_lhs 2 3 => rw [plusCompIso_whiskerRight]
-- 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 (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
        (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
            (CategoryStruct.comp (Y := J.plusObj (P ⋙ F))
                (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
                (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F)) :
              J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj P ⋙ F))
            (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
          J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
      P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
    (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
have rw : Eq (α := P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (CategoryStruct.comp (Y := J.plusObj P ⋙ F) (whiskerRight (J.toPlus P) F : P ⋙ F ⟶ J.plusObj P ⋙ F)
      (CategoryStruct.comp (Y := J.plusObj (P ⋙ F)) (Iso.hom (J.plusCompIso F P) : J.plusObj P ⋙ F ⟶ J.plusObj (P ⋙ F))
          (CategoryStruct.comp (Y := J.plusObj (J.plusObj P ⋙ F))
              (J.plusMap (whiskerRight (J.toPlus P) F) : J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj P ⋙ F))
              (J.plusMap (Iso.hom (J.plusCompIso F P)) : J.plusObj (J.plusObj P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
            J.plusObj (P ⋙ F) ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
        J.plusObj P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F))) :
    P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
  (J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) : P ⋙ F ⟶ J.plusObj (J.plusObj (P ⋙ F)))
Tactic: rw [Category.assoc, ← J.plusMap_comp, whiskerRight_toPlus_comp_plusCompIso_hom, ←
    Category.assoc, whiskerRight_toPlus_comp_plusCompIso_hom]
-- 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 (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
        (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
      P ⋙ F ⟶ J.sheafify P ⋙ F)
    (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
have rw : Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
  (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
      (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
    P ⋙ F ⟶ J.sheafify (P ⋙ F))
Tactic: rw [Iso.comp_inv_eq]
-- 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
FD : D → D → Type u_3
CD : D → Type u_4
inst_9 : (X Y : D) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : ConcreteCategory.{u_4, v_1, u_1, u_3} D FD (CC := CD)
inst_11 : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_13 : ReflectsIsomorphisms.{v_1, u_1, u_4, u_4 + 1} (forget D (FC := FD) (CC := CD))
⊢ Eq (α := J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
    (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
    (J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯ : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F)
have a : Eq (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
  (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
      (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
    P ⋙ F ⟶ J.sheafify P ⋙ F)
  (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
Tactic: apply J.sheafifyLift_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 : Functor.{v, v_1, u, u_1} Cᵒᵖ D
FD : D → D → Type u_3
CD : D → Type u_4
inst_9 : (X Y : D) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FD X Y) (CD X) (CD Y)
inst_10 : ConcreteCategory.{u_4, v_1, u_1, u_3} D FD (CC := CD)
inst_11 : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D (FC := FD) (CC := CD))
inst_12 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_13 : ReflectsIsomorphisms.{v_1, u_1, u_4, u_4 + 1} (forget D (FC := FD) (CC := CD))
⊢ Eq (α := P ⋙ F ⟶ J.sheafify P ⋙ F)
    (CategoryStruct.comp (Y := J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
        (Iso.inv (J.sheafifyCompIso F P) : J.sheafify (P ⋙ F) ⟶ J.sheafify P ⋙ F) :
      P ⋙ F ⟶ J.sheafify P ⋙ F)
    (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
have a : Eq (α := P ⋙ F ⟶ J.sheafify (P ⋙ F)) (J.toSheafify (P ⋙ F) : P ⋙ F ⟶ J.sheafify (P ⋙ F))
  (CategoryStruct.comp (Y := J.sheafify P ⋙ F) (whiskerRight (J.toSheafify P) F : P ⋙ F ⟶ J.sheafify P ⋙ F)
      (Iso.hom (J.sheafifyCompIso F P) : J.sheafify P ⋙ F ⟶ J.sheafify (P ⋙ F)) :
    P ⋙ F ⟶ J.sheafify (P ⋙ F))
Tactic: rw [Iso.comp_inv_eq]
-- 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)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S : Sieve X).arrows f
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow } =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := g, hf := ⋯ }
have subst : (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf : S.Arrow } =
  (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := sorry }
Tactic: subst h
Cleared hypotheses: g, 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)
Y X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
f : Y ⟶ X
⊢ Eq (α := CD ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD ((J.plusObj P).obj (op Y)))
    (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) f) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op Y)))
have dsimp : Eq.{t + 1} (α := CD (colimit (J.diagram P Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (CategoryStruct.comp (Y := colimit ((J.pullback f).op ⋙ J.diagram P Y)) (colimMap (J.diagramPullback P f))
            (colimit.pre (J.diagram P Y) (J.pullback f).op)) :
        (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P Y)))
      ((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))) x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
        CD (colimit (J.diagram P X))) :
    CD (colimit (J.diagram P Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) (op (S.pullback f))) :
        (a : CD (multiequalizer ((S.pullback f).index P))) → CD (colimit (J.diagram P Y)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
            (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
          (x.pullback (FD := FD) (CD := CD) f) :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer ((S.pullback f).index P))) :
    CD (colimit (J.diagram P Y)))
Tactic: dsimp [mk, 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)
Y X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
f : Y ⟶ X
⊢ Eq.{t + 1} (α := CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))) :
          (a : CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S))) → CD (colimit (J.diagram P Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P f) (op S)) :
              (a : CD (multiequalizer (S.index P))) → CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
            ((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 (((J.pullback f).op ⋙ J.diagram P Y).obj (op S))) :
      CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) (op (S.pullback f))) :
          (a : CD (multiequalizer ((S.pullback f).index P))) → CD (colimit (J.diagram P Y)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
              (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
            (x.pullback (FD := FD) (CD := CD) f) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer ((S.pullback f).index P))) :
      CD (colimit (J.diagram P Y)))
have h : Eq.{t + 1} (α := CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P f) (op S)) :
        (a : CD (multiequalizer (S.index P))) → CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
      ((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 (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
  ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
        (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
      (x.pullback (FD := FD) (CD := CD) f) :
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer ((S.pullback f).index P)))
Tactic: apply congr_arg