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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S : Sieve X).arrows e2
he1 :
  Sieve.arrows
    ((fun (Y : C) (f : Y ⟶ X) (hf : (↑S : Sieve X).arrows f) ↦
        ((↑(W { 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))
      Z e2 he2)
    e1
hee : e1 ≫ e2 = f
⊢ (↑Sx : Sieve X).arrows f
have rw : (↑Sx : Sieve X).arrows (e1 ≫ e2)
Tactic: rw [← hee]
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S : Sieve X).arrows e2
he1 :
  Sieve.arrows
    ((fun (Y : C) (f : Y ⟶ X) (hf : (↑S : Sieve X).arrows f) ↦
        ((↑(W { 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))
      Z e2 he2)
    e1
hee : e1 ≫ e2 = f
⊢ (↑Sy : Sieve X).arrows f
have rw : (↑Sy : Sieve X).arrows (e1 ≫ e2)
Tactic: rw [← hee]
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
⊢ ∃ (h1 : B ⟶ Sx) (h2 : B ⟶ Sy), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
have h₁ : x.refine (FD := FD) (CD := CD) ex = y.refine (FD := FD) (CD := CD) ey
Tactic: use ex, ey
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
⊢ x.refine (FD := FD) (CD := CD) ex = y.refine (FD := FD) (CD := CD) ey
have h₁ : ∀ (I : B.Arrow),
  (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I
Tactic: ext1 I
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (hypothesis)
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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
I : B.Arrow
IS : S.Arrow := I.fromMiddle
⊢ (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I
have hh₁ : (x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS) =
  (y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)
Tactic: specialize hh IS
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (hypothesis)
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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
I : B.Arrow
IS : S.Arrow := I.fromMiddle
hh :
  (x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS) =
    (y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)
IW : (W IS).Arrow := I.toMiddle
⊢ (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I
have hh₁ : (↑((x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS)) :
      (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
    IW =
  (↑((y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)) :
      (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
    IW
Tactic: apply_fun fun e => e IW at hh
Cleared hypotheses: hh
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
I : B.Arrow
IS : S.Arrow := I.fromMiddle
IW : (W IS).Arrow := I.toMiddle
hh :
  (↑((x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW =
    (↑((y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW
⊢ (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I
have h₁ : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.Y)) =
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op IW.Y)) →
  (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑((x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW
Tactic: convert! hh using 1
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
ey : B ⟶ Sy := homOfLE ⋯
I : B.Arrow
IS : S.Arrow := I.fromMiddle
IW : (W IS).Arrow := I.toMiddle
hh :
  (↑((x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW =
    (↑((y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW
h₁ :
  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.Y)) =
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op IW.Y)) →
    (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
      (↑((x.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h1 IS)) :
          (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
        IW
⊢ (↑(x.refine (FD := FD) (CD := CD) ex) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I
have h₂ : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.Y)) =
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op IW.Y)) →
  (↑(y.refine (FD := FD) (CD := CD) ey) : (I : B.Arrow) → ToType (P.obj (op I.Y))) I =
    (↑((y.pullback (FD := FD) (CD := CD) IS.f).refine (FD := FD) (CD := CD) (h2 IS)) :
        (I : (W IS).Arrow) → ToType (P.obj (op I.Y)))
      IW
Tactic: convert! hh using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (hypothesis)
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
x y : CD (P.obj (op X))
h :
  Eq (α := 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)))
        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)))
        y :
      CD ((J.plusObj P).obj (op X)))
⊢ x = y
have h₁ : Eq (α := CD ((J.plusObj P).obj (op X)))
  (mk (FD := FD) (CD := CD) (S := ⊤) (Meq.mk (FD := FD) (CD := CD) ⊤ x) :
    ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
  (mk (FD := FD) (CD := CD) (S := ⊤) (Meq.mk (FD := FD) (CD := CD) ⊤ y))
Tactic: simp only [toPlus_eq_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (hypothesis)
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
x y : CD (P.obj (op X))
h :
  Eq (α := CD ((J.plusObj P).obj (op X)))
    (mk (FD := FD) (CD := CD) (S := ⊤) (Meq.mk (FD := FD) (CD := CD) ⊤ x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
    (mk (FD := FD) (CD := CD) (S := ⊤) (Meq.mk (FD := FD) (CD := CD) ⊤ y))
⊢ x = y
have h₁ : ∃ (W : J.Cover X) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
  Eq (α := Meq (FD := FD) (CD := CD) P W) (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ x) h1)
    (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ y) h2)
Tactic: rw [eq_mk_iff_exists] at h
Cleared hypotheses: h
-- 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
x y : CD (P.obj (op X))
h :
  ∃ (W : J.Cover X) (h1 : W ⟶ ⊤) (h2 : W ⟶ ⊤),
    Eq (α := Meq (FD := FD) (CD := CD) P W) (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ x) h1)
      (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ y) h2)
⊢ x = y
have obtain : ∀ (W : J.Cover X) (h1 h2 : W ⟶ ⊤)
  (hh :
    Eq (α := Meq (FD := FD) (CD := CD) P W) (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ x) h1)
      (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ y) h2)),
  x = y
Tactic: obtain ⟨W, h1, h2, hh⟩ := h
Cleared hypotheses: h
-- 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
x y : CD (P.obj (op X))
W : J.Cover X
h1 h2 : W ⟶ ⊤
hh :
  Eq (α := Meq (FD := FD) (CD := CD) P W) (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ x) h1)
    (Meq.refine (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) ⊤ y) h2)
⊢ x = y
have a : ∀ (I : W.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)))
Tactic: apply hsep X W