-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toPlus_apply {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : Meq P S) (I : S.Arrow) :
    (J.toPlus P).app _ (x I) = (J.plusObj P).map I.f.op (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
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ⊤)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯)) (↑x I)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Tactic:
rw [← colimit.w _ e.op, 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
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))))
      ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Proof state:
case h.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
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ ∀ (t : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L),
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t))
        ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
          ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯))
            (↑x I))) =
      (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t))
        ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Tactic:
intro i

Result:
case h.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
S : J.Cover X
x : Meq 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
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) i))
      ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) i))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm 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
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))))
      ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm 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
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯)) (↑x I)) =
    (ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm 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
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤))) (↑x I) =
    (ConcreteCategory.hom
        (colimMap (J.diagramPullback P I.f.op.unop) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op))
      (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
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯ ≫
          colimit.ι (J.diagram P I.Y) (op ⊤)))
      (↑x I) =
    (ConcreteCategory.hom
        (colimMap (J.diagramPullback P I.f.op.unop) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op))
      (mk x)