awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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.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
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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.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:
hh
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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
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
⊢ (↑(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:
convert! hh using 1
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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
e_1 :
  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:
x.congr_apply I.middle_spec.symm _

Premises used: CategoryTheory.Meq.congr_apply, CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom, CategoryTheory.GrothendieckTopology.Cover, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom, Classical.choose, Eq.symm, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle, CategoryTheory.GrothendieckTopology.Cover.bind, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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
e_1 :
  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:
exact x.congr_apply I.middle_spec.symm _

Premises used: CategoryTheory.Meq.congr_apply, Eq.symm, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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
e_1 :
  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:
y.congr_apply I.middle_spec.symm _

Premises used: CategoryTheory.Meq.congr_apply, CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom, CategoryTheory.GrothendieckTopology.Cover, CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom, Classical.choose, Eq.symm, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle, CategoryTheory.GrothendieckTopology.Cover.bind, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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
e_1 :
  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:
exact y.congr_apply I.middle_spec.symm _

Premises used: CategoryTheory.Meq.congr_apply, Eq.symm, CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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)))
⊢ 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

Premises used: CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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))
⊢ ∃ (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

Premises used: CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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)
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
⊢ x = y

Tactic:
obtain ⟨W, h1, h2, hh⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
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)
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)))
⊢ x = y

Tactic:
apply hsep X W