-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toPlus_eq_mk {X : C} {P : Cᵒᵖ ⥤ D} (x : ToType (P.obj (op X))) :
    (J.toPlus P).app _ x = mk (Meq.mk ⊤ x)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯ ≫ colimit.ι (J.diagram P X) (op ⊤)))
      x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Tactic:
simp only [ConcreteCategory.comp_apply]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Proof state:
case h.a
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (Meq.equiv P ⊤)
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x) =
    (Meq.equiv P ⊤) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Tactic:
ext i

Result:
case h.a.h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
i : ⊤.Arrow
⊢ ↑((Meq.equiv P ⊤)
          ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x))
      i =
    ↑((Meq.equiv P ⊤) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))) i

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Tactic:
apply congr_arg

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x =
    (Meq.equiv P ⊤).symm (Meq.mk ⊤ x)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op X))) x = mk (Meq.mk ⊤ x)

Tactic:
dsimp [mk, toPlus]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))

Tactic:
delta Cover.toMultiequalizer

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯ ≫ colimit.ι (J.diagram P X) (op ⊤)))
      x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op ⊤))) ((Meq.equiv P ⊤).symm (Meq.mk ⊤ x))