-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
left :
  Function.Injective (α :=
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))))
    (β :=
    (fun (X : Type t) ↦ X)
      (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P)))) :
      (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
        (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
⊢ Function.Bijective (α :=
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))))
    (β :=
    (fun (X : Type t) ↦ X)
      (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P)))) :
      (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
        (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
have right : Function.Surjective (α :=
  (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))))
  (β :=
  (fun (X : Type t) ↦ X)
    (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P)))) :
    (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
      (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
Tactic: constructor