awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
s : Meq (FD := FD) (CD := CD) (J.plusObj P) S
inj :
  ∀ (X : C),
    Function.Injective.{t + 1, t + 1} (α := CD (P.obj (op X))) (β := CD ((J.plusObj P).obj (op X)))
      (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op X))) :
        (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq (FD := FD) (CD := CD) P (T I)
ht : ∀ (I : S.Arrow), (↑s : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) I = mk (FD := FD) (CD := CD) (t I)
B : J.Cover X := S.bind T
Z : (I : B.Arrow) → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S : Sieve X).arrows (e2 I)
h :
  ∀ (I : B.Arrow),
    (fun (x : C) (x_1 : x ⟶ X) (h : (↑S : Sieve X).arrows x_1) ↦
        (Sieve.arrows
            ((fun (Y : C) (f : Y ⟶ X) (hf : (↑S : Sieve X).arrows f) ↦
                ((↑(T { Y := Y, f := f, hf := hf : S.Arrow }) : Sieve.{v, u} { Y := Y, f := f, hf := hf : S.Arrow }.Y) :
                  Sieve.{v, u} { Y := Y, f := f, hf := hf : S.Arrow }.Y))
              x x_1 h) :
          Presieve.{v, u} x))
      (Z I) (e2 I) ⋯ (e1 I)
h_1 : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq (FD := FD) (CD := CD) P B := meqOfSep (FD := FD) (CD := CD) P hsep X S s T t ht
I : S.Arrow
II : (T I).Arrow
Y : C
f : Y ⟶ II.Y
hf : (↑((J.pullback II.f).obj (T I)) : Sieve II.Y).arrows f
⊢ (↑((J.pullback II.f).obj ((J.pullback I.f).obj B)) : Sieve II.Y).arrows f
have a : Sieve.arrows (↑(T { Y := I.Y, f := I.f, hf := sorry : S.Arrow }) : Sieve { Y := I.Y, f := I.f, hf := sorry }.Y) (f ≫ II.f)
Tactic: apply Sieve.le_pullback_bind _ _ _ I.hf
-- 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
⊢ Presheaf.IsSheaf J (J.plusObj P)
have rw : ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index (J.plusObj P))) (S.toMultiequalizer (J.plusObj P))
Tactic: rw [Presheaf.isSheaf_iff_multiequalizer]
-- 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
⊢ IsIso (Y := multiequalizer (S.index (J.plusObj P))) (S.toMultiequalizer (J.plusObj P))
have apply : IsIso (X := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))) (Y :=
  Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P))))
  (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P)))
Tactic: apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (forget D) ?_
-- 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
⊢ IsIso (X := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))) (Y :=
    Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P))))
    (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P)))
have rw : 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)))))
Tactic: rw [isIso_iff_bijective]
-- 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
⊢ 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 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)))))
Tactic: constructor
-- 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
x y : Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))
h :
  Eq (α :=
    (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)))))
        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)))))
        y :
      (fun (X : Type t) ↦ X)
        (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
⊢ x = y
have left : ∀ (I : S.Arrow),
  Eq (α := CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
        x :
      CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
        y :
      CD ((J.plusObj P).obj (op I.Y)))
Tactic: apply sep P S _ _
-- 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
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
⊢ ∃ (a :
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
    (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)))))
        a =
      x
have right : ∀ (t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
  (ht :
    Meq.mk (FD := FD) (CD := CD) S t =
      (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
          (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
        x),
  ∃ (a :
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
    (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)))))
        a =
      x
Tactic: obtain ⟨t, ht⟩ := exists_of_sep P hsep X S (Meq.equiv _ _ x)
-- 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
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
⊢ ∃ (a :
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
    (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)))))
        a =
      x
have h : (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)))))
    t =
  x
Tactic: use t
-- 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
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
⊢ (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)))))
      t =
    x
have h : Eq (α := Meq (FD := FD) (CD := CD) (J.plusObj P) S)
  ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      ((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)))))
        t) :
    Meq (FD := FD) (CD := CD) (J.plusObj P) S)
  ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x :
    Meq (FD := FD) (CD := CD) (J.plusObj P) S)
Tactic: apply (Meq.equiv (D := D) _ _).injective