-- 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:
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

Tactic:
rw [Meq.equiv_apply, Equiv.apply_symm_apply, ← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]

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
⊢ (ConcreteCategory.hom (P.map i.f.op)) x = ↑(Meq.mk ⊤ x) i

Proof state:
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
⊢ (ConcreteCategory.hom (P.map i.f.op)) x = ↑(Meq.mk ⊤ x) i

Tactic:
rfl

Result:
no goals

Proof state:
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)

Tactic:
apply (Meq.equiv P ⊤).injective

Result:
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))