-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem exists_rep {X : C} {P : Cᵒᵖ ⥤ D} (x : ToType ((J.plusObj P).obj (op X))) :
    ∃ (S : J.Cover X) (y : Meq P S), x = mk y

Proof state:
case intro.intro
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ ∃ S y, x = mk y

Tactic:
use S.unop, Meq.equiv _ _ y

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ x = mk ((Meq.equiv P (unop S)) y)

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
⊢ ∃ S y, x = mk y

Tactic:
obtain ⟨S, y, h⟩ := Concrete.colimit_exists_rep (J.diagram P X) x

Result:
case intro.intro
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ ∃ S y, x = mk y

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ x = mk ((Meq.equiv P (unop S)) y)

Tactic:
rw [← h]

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = mk ((Meq.equiv P (unop S)) y)

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = mk ((Meq.equiv P (unop S)) y)

Tactic:
dsimp [mk]

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) ((Meq.equiv P (unop S)).symm ((Meq.equiv P (unop S)) y))

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) ((Meq.equiv P (unop S)).symm ((Meq.equiv P (unop S)) y))

Tactic:
simp

Result:
no goals