awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
heq :
  ∀ (s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j)
    (hab : a ≫ c.inj i = b ≫ c.inj j),
    Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          a :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          b :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
m :
  Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ J.yoneda.obj (X i))
      (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i)) ⟶
    s.pt
hm :
  ∀ (j : ι),
    Cofan.inj (f := fun (i : ι) ↦ J.yoneda.obj (X i))
          (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i)) j ≫
        m =
      s.inj j
refine_3 :
  (Sieve.ofArrows X c.inj).functorInclusion ≫ m.hom =
    {
      app := fun (Y : Cᵒᵖ) ↦
        ↾fun
            (g :
              { g : unop Y ⟶ c.pt //
                ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt), Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
              (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
            (Sieve.ofArrows.h ⋯),
      naturality := ⋯ }
⊢ m.hom =
    ⋯.extend
      {
        app := fun (Y : Cᵒᵖ) ↦
          ↾fun
              (g :
                { g : unop Y ⟶ c.pt //
                  ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt), Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
              (Sieve.ofArrows.h ⋯),
        naturality := ⋯ }

Tactic:
apply Presieve.IsSheafFor.unique_extend

Premises used: CategoryTheory.Presieve.IsSheafFor.unique_extend
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan.{u_1, v, u} X
H : Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
inst_2 : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
hdisj :
  ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial.{v, u} Y)
heq :
  ∀ (s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j)
    (hab : a ≫ c.inj i = b ≫ c.inj j),
    Eq (α := (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj i).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X i)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          a :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((s.inj j).hom.app (op Y)) :
            (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (X j)).obj.obj (op Y))) →
              (fun (X : Type v) ↦ X) (s.pt.obj.obj (op Y)))
          b :
        (fun (X : Type v) ↦ X) (s.pt.obj (P := Presheaf.IsSheaf J).obj (op Y)))
s : Cofan (C := Sheaf J (Type v)) fun (i : ι) ↦ J.yoneda.obj (X i)
m :
  Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ J.yoneda.obj (X i))
      (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i)) ⟶
    s.pt
hm :
  ∀ (j : ι),
    Cofan.inj (f := fun (i : ι) ↦ J.yoneda.obj (X i))
          (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i)) j ≫
        m =
      s.inj j
Y : Cᵒᵖ
g : unop Y ⟶ c.pt
hg : (Sieve.ofArrows X c.inj).arrows g
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (((Sieve.ofArrows X c.inj).functorInclusion ≫ m.hom).app Y)).toFun
      (Subtype.mk (p := fun (g : unop Y ⟶ c.pt) ↦ (Sieve.ofArrows X c.inj).arrows g) g hg) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          {
            app := fun (Y : Cᵒᵖ) ↦
              ↾fun
                  (g :
                    { g : unop Y ⟶ c.pt //
                      ∃ (Y_1 : C) (h : unop Y ⟶ Y_1) (g_1 : Y_1 ⟶ c.pt),
                        Presieve.ofArrows X c.inj g_1 ∧ h ≫ g_1 = g }) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app (InducedCategory.Hom.hom (s.inj (Sieve.ofArrows.i ⋯))) Y) :
                    (a : unop Y ⟶ X (Sieve.ofArrows.i ⋯)) → s.pt.obj.obj Y)
                  (Sieve.ofArrows.h ⋯),
            naturality := ⋯ : NatTrans (Sieve.ofArrows X c.inj).functor (s.pt.obj (P := Presheaf.IsSheaf J)) }
          Y))
      (Subtype.mk (p := fun (g : unop Y ⟶ c.pt) ↦ (Sieve.ofArrows X c.inj).arrows g) g hg)

Tactic:
simp [← hm (Sieve.ofArrows.i hg)]

Premises used: CategoryTheory.Sieve.ofArrows.i
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst_1 : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_2 : J.Subcanonical
ι : Type u_1
inst_3 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
inst : ∀ (f : ι → C), PreservesColimit (Discrete.functor f) J.yoneda
⊢ PreservesColimitsOfShape (Discrete ι) J.yoneda

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_of_discrete

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_discrete
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
inst_2 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
⊢ ∀ (f : ι → C), PreservesColimit (Discrete.functor f) J.yoneda

Tactic:
fun X ↦ ⟨fun {c : Cofan X} hc ↦ ⟨(Limits.Cofan.isColimitMapCoconeEquiv _ _ _).symm ?_⟩⟩

Premises used: CategoryTheory.GrothendieckTopology.yoneda, Nonempty.intro, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst_1 : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_2 : J.Subcanonical
ι : Type u_1
inst_3 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
inst :
  (X : ι → C) →
    {c : Cofan.{u_1, v, u} X} →
      (hc : IsColimit c) →
        IsColimit (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ J.yoneda.obj (X i))
          (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i))
⊢ ∀ (f : ι → C), PreservesColimit (Discrete.functor f) J.yoneda

Tactic:
refine fun X ↦ ⟨fun {c : Cofan X} hc ↦ ⟨(Limits.Cofan.isColimitMapCoconeEquiv _ _ _).symm ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
inst_2 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
⊢ ∀ (i : ι), Mono (c.inj i)

Tactic:
have (i : ι) : Mono (c.inj i) := .of_coproductDisjoint hc _
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst_1 : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_2 : J.Subcanonical
ι : Type u_1
inst_3 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_4 : HasPullbacks.{v, u} C
inst_5 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : ∀ (i : ι), Mono (c.inj i)
inst :
  {i j : ι} →
    (hij : i ≠ j) → (Y : C) → (a : Y ⟶ X i) → (b : Y ⟶ X j) → (hab : a ≫ c.inj i = b ≫ c.inj j) → IsInitial.{v, u} Y
⊢ IsColimit (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ J.yoneda.obj (X i))
    (Cofan.mk (J.yoneda.obj c.pt) fun (i : ι) ↦ J.yoneda.map (c.inj i))

Tactic:
refine isColimitCofanMkYoneda _ _ (hcov hc) htriv fun hij Y a b hab ↦ ⟨?_⟩

Premises used: Nonempty.intro, CategoryTheory.GrothendieckTopology.isColimitCofanMkYoneda
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
ι : Type u_1
inst_2 : CoproductsOfShapeDisjoint.{v, u, u_1} C ι
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasStrictInitialObjects.{v, u} C
hcov :
  ∀ {X : ι → C} {c : Cofan.{u_1, v, u} X} (x : IsColimit c),
    Membership.mem (γ := Set (Sieve.{v, u} c.pt)) ((J : (a : C) → Set (Sieve a)) c.pt) (Sieve.ofArrows X c.inj)
htriv : ∀ (Y : C) (a : IsInitial.{v, u} Y), ⊥ ∈ (J : (a : C) → Set (Sieve a)) Y
X : ι → C
c : Cofan.{u_1, v, u} X
hc : IsColimit c
this : ∀ (i : ι), Mono (c.inj i)
i j : ι
hij : i ≠ j
Y : C
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
⊢ IsInitial.{v, u} Y

Tactic:
exact .ofCoproductDisjointOfCommSq hij hc _ _ hab
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
⊢ J.Subcanonical

Tactic:
.of_isSheaf_yoneda_obj _ fun Y ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
refine : ∀ (Y : C), Presieve.IsSheaf J (obj CategoryTheory.yoneda Y)
⊢ J.Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun Y ↦ ?_
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (obj CategoryTheory.uliftYoneda.{v', v, u} Y)
e : ⦃X : C⦄ → obj (obj CategoryTheory.yoneda Y) (op X) ≃ obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X)
he :
  ∀ ⦃X Y_1 : C⦄ (f : X ⟶ Y_1) (x : obj (obj CategoryTheory.yoneda Y) (op Y_1)),
    Eq (α := obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X))
      ((Equiv.symm Equiv.ulift :
            (a : (CategoryTheory.yoneda.obj Y).obj (op X)) → (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj CategoryTheory.yoneda Y) f.op) :
              (a : (fun (X : Type v) ↦ X) ((CategoryTheory.yoneda.obj Y).obj (op Y_1))) →
                (fun (X : Type v) ↦ X) ((CategoryTheory.yoneda.obj Y).obj (op X)))
            x) :
        obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj CategoryTheory.uliftYoneda.{v', v, u} Y) f.op) :
            (a : (fun (X : Type (max v v')) ↦ X) ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op Y_1))) →
              (fun (X : Type (max v v')) ↦ X) ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X)))
          ((Equiv.symm Equiv.ulift :
              (a : (CategoryTheory.yoneda.obj Y).obj (op Y_1)) →
                (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op Y_1))
            x) :
        (fun (X : Type (max v v')) ↦ X) (obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X)))
⊢ Presieve.IsSheaf J (obj CategoryTheory.yoneda Y)

Tactic:
rwa [Presieve.isSheaf_iff_of_nat_equiv]

Premises used: CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (obj CategoryTheory.uliftYoneda.{v', v, u} Y)
X : C
⊢ obj (obj CategoryTheory.yoneda Y) (op X) ≃ obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X)

Tactic:
exact Equiv.ulift.symm

Premises used: Equiv.ulift, Equiv.symm
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (obj CategoryTheory.uliftYoneda.{v', v, u} Y)
X Y_1 : C
f : X ⟶ Y_1
x : obj (obj CategoryTheory.yoneda Y) (op Y_1)
⊢ Eq (α := obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X))
    ((Equiv.symm Equiv.ulift :
          (a : (CategoryTheory.yoneda.obj Y).obj (op X)) → (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj CategoryTheory.yoneda Y) f.op) :
            (a : (fun (X : Type v) ↦ X) ((CategoryTheory.yoneda.obj Y).obj (op Y_1))) →
              (fun (X : Type v) ↦ X) ((CategoryTheory.yoneda.obj Y).obj (op X)))
          x) :
      obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj CategoryTheory.uliftYoneda.{v', v, u} Y) f.op) :
          (a : (fun (X : Type (max v v')) ↦ X) ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op Y_1))) →
            (fun (X : Type (max v v')) ↦ X) ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X)))
        ((Equiv.symm Equiv.ulift :
            (a : (CategoryTheory.yoneda.obj Y).obj (op Y_1)) →
              (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op Y_1))
          x) :
      (fun (X : Type (max v v')) ↦ X) (obj (obj CategoryTheory.uliftYoneda.{v', v, u} Y) (op X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
suffices : Presieve.IsSheaf J (obj CategoryTheory.uliftYoneda.{v', v, u} Y)
⊢ Presieve.IsSheaf J (obj CategoryTheory.yoneda Y)

Tactic:
suffices h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v'}.obj Y) by
    rwa [Presieve.isSheaf_iff_of_nat_equiv]
    · intro
      exact Equiv.ulift.symm
    · intros
      rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
rw :
  Presheaf.IsSheaf J
    ((F ⋙ CategoryTheory.uliftYoneda.{v, v', u_1} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v v'))) F.op).obj Y)
⊢ Presieve.IsSheaf J (obj CategoryTheory.uliftYoneda.{v', v, u} Y)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type, Presheaf.isSheaf_of_iso_iff
    ((Functor.FullyFaithful.ofFullyFaithful F).compUliftYonedaCompWhiskeringLeft.app Y).symm]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Iso.symm, CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft, CategoryTheory.Iso.app, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
⊢ Presheaf.IsSheaf J
    ((F ⋙ CategoryTheory.uliftYoneda.{v, v', u_1} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v v'))) F.op).obj Y)

Tactic:
F.op_comp_isSheaf_of_isSheaf J K _ ?_

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf, CategoryTheory.Functor.comp
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
refine : Presheaf.IsSheaf K (obj CategoryTheory.uliftYoneda.{v, v', u_1} (F.obj Y))
⊢ Presheaf.IsSheaf J
    ((F ⋙ CategoryTheory.uliftYoneda.{v, v', u_1} ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v v'))) F.op).obj Y)

Tactic:
refine F.op_comp_isSheaf_of_isSheaf J K _ ?_

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
rw : Presieve.IsSheaf K (obj CategoryTheory.uliftYoneda.{v, v', u_1} (F.obj Y))
⊢ Presheaf.IsSheaf K (obj CategoryTheory.uliftYoneda.{v, v', u_1} (F.obj Y))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v', u_1} D
F : Functor.{v, v', u, u_1} C D
J : GrothendieckTopology.{v, u} C
K : GrothendieckTopology.{v', u_1} D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.IsContinuous J K
inst_5 : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf K (obj CategoryTheory.uliftYoneda.{v, v', u_1} (F.obj Y))

Tactic:
apply GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
⊢ (J.over X).Subcanonical

Tactic:
.of_isSheaf_yoneda_obj _ fun E Z R hR t ht ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
refine :
  ∀ (E Z : Over.{v_1, u_1} X) (R : Sieve Z) (hR : R ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z)
    (t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) R.arrows) (ht : t.Compatible (R := R.arrows)),
    ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z), t.IsAmalgamation (R := R.arrows) t_1
⊢ (J.over X).Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun E Z R hR t ht ↦ ?_
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
R : Sieve Z
hR : R ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) R.arrows
ht : t.Compatible (R := R.arrows)
obtain :
  ∀ (ι : Type (max u_1 v_1)) (T : ι → Over.{v_1, u_1} X) (g : (i : ι) → T i ⟶ Z)
    (hR : Sieve.ofArrows T g ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z)
    (t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows)
    (ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)),
    ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
      t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1
⊢ ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z), t.IsAmalgamation (R := R.arrows) t_1

Tactic:
obtain ⟨ι, T, g, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Sieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z_1 : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z_1
hR : Sieve.ofArrows T g ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z_1
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : Eq (α := Z ⟶ Z_1.left) (gi ≫ (fun (i : ι) ↦ Over.Hom.left (g i)) i) (gj ≫ (fun (i : ι) ↦ Over.Hom.left (g i)) j)
dsimp : gj ≫ (T j).hom = gi ≫ (T i).hom
⊢ gj ≫ (T j).hom = (Over.mk (gi ≫ (T i).hom)).hom

Tactic:
dsimp