awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : C
H : ⊥ ∈ (J : (a : C) → Set (Sieve a)) X
Y : A
t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)
h :
  (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
        Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
          (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
      t ∧
    ∀ (y : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)),
      (fun (t : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op X)) ↦
            Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥)
              (fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯) t)
          y →
        y = t
⊢ Unique (Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
exact ⟨⟨t⟩, fun a => h.2 a (by tauto)⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
X : A
hX : IsTerminal.{v₂, u₂} X
X_1 : Sheaf.{v₁, v₂, u₁, u₂} J A
m : X_1 ⟶ terminal J hX
h :
  ∀ (x : Cᵒᵖ),
    m.hom.app x =
      NatTrans.app
        (InducedCategory.Hom.hom
          ((fun (x : Sheaf.{v₁, v₂, u₁, u₂} J A) ↦
              ({ hom := IsTerminal.from (Functor.isTerminalConst Cᵒᵖ hX) (x.obj (P := Presheaf.IsSheaf J)) } :
                InducedCategory.Hom (D := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F :=
                  ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) x (terminal J hX)))
            X_1))
        x
⊢ m =
    (fun (x : Sheaf.{v₁, v₂, u₁, u₂} J A) ↦
        ({ hom := IsTerminal.from (Functor.isTerminalConst Cᵒᵖ hX) (x.obj (P := Presheaf.IsSheaf J)) } :
          InducedCategory.Hom (D := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F :=
            ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) x (terminal J hX)))
      X_1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
X : A
hX : IsTerminal.{v₂, u₂} X
X_1 : Sheaf.{v₁, v₂, u₁, u₂} J A
m : X_1 ⟶ terminal J hX
x : Cᵒᵖ
⊢ m.hom.app x =
    NatTrans.app
      (InducedCategory.Hom.hom
        ((fun (x : Sheaf.{v₁, v₂, u₁, u₂} J A) ↦
            ({ hom := IsTerminal.from (Functor.isTerminalConst Cᵒᵖ hX) (x.obj (P := Presheaf.IsSheaf J)) } :
              InducedCategory.Hom (D := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (F :=
                ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) x (terminal J hX)))
          X_1))
      x

Tactic:
simpa using hX.hom_ext _ _

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
X : A
hX : IsTerminal.{v₂, u₂} X
G : Sheaf.{v₁, v₂, u₁, u₂} J A
⊢ ((isTerminalTerminal J hX).from G).hom =
    IsTerminal.from (Functor.isTerminalConst Cᵒᵖ hX) (G.obj (P := Presheaf.IsSheaf J))

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf.{v₁, v₂, u₁, u₂} J A
refine : IsTerminal (Functor.obj (sheafToPresheaf J A) F)
⊢ IsTerminal F

Tactic:
refine IsTerminal.isTerminalOfObj (sheafToPresheaf _ _) _ ?_

Premises used: CategoryTheory.Limits.IsTerminal.isTerminalOfObj, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf.{v₁, v₂, u₁, u₂} J A
refine : ∀ (X : Cᵒᵖ), Membership.mem (γ := Set (Sieve.{v₁, u₁} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) ⊥
⊢ IsTerminal (Functor.obj (sheafToPresheaf J A) F)

Tactic:
refine Functor.isTerminal fun X ↦ Sheaf.isTerminalOfBotCover _ _ ?_

Premises used: CategoryTheory.Functor.isTerminal, CategoryTheory.Sheaf.isTerminalOfBotCover, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
H : J = ⊤
F : Sheaf.{v₁, v₂, u₁, u₂} J A
X : Cᵒᵖ
⊢ Membership.mem (γ := Set (Sieve.{v₁, u₁} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) ⊥

Tactic:
simp [H]
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : Preadditive.{v₂, u₂} A
P Q : Sheaf.{v₁, v₂, u₁, u₂} J A
f g : P ⟶ Q
U : Cᵒᵖ
⊢ (f + g).hom.app U = f.hom.app U + g.hom.app U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
a : S.shape.L
⊢ Eq (α := E.pt ⟶ (S.index P).multicospan.obj (WalkingMulticospan.left a))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left a))
    (E.π.app (WalkingMulticospan.left a))

Tactic:
apply hP.amalgamate_map

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
right :
  (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b))) ≫
      (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
⊢ Eq (α := E.pt ⟶ (S.index P).multicospan.obj (WalkingMulticospan.right b))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b))
    (E.π.app (WalkingMulticospan.right b))

Tactic:
rw [← E.w (WalkingMulticospan.Hom.fst b),
        ← (S.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.Cover.multifork, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingMulticospan.Hom.fst
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
right :
  Eq (α := E.pt ⟶ (S.index P).multicospan.obj (WalkingMulticospan.left (S.shape.fst b)))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b)))
    (E.π.app (WalkingMulticospan.left (S.shape.fst b)))
⊢ (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b))) ≫
      (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ Eq (α := E.pt ⟶ (S.index P).multicospan.obj (WalkingMulticospan.left (S.shape.fst b)))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b)))
    (E.π.app (WalkingMulticospan.left (S.shape.fst b)))

Tactic:
apply hP.amalgamate_map

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
h : ∀ (I : S.Arrow), m ≫ P.map I.f.op = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op
⊢ m = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯

Tactic:
apply hP.hom_ext S

Premises used: CategoryTheory.Presheaf.IsSheaf.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
h :
  Eq (α := E.pt ⟶ P.obj (op I.Y))
    (E.π.app (WalkingMulticospan.left I) :
      Functor.obj (C := WalkingMulticospan S.shape) (Functor.obj (Functor.const (WalkingMulticospan S.shape)) E.pt)
          (WalkingMulticospan.left I) ⟶
        (S.index P).multicospan.obj (WalkingMulticospan.left I))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op)
⊢ m ≫ P.map I.f.op = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op

Tactic:
erw [hm (WalkingMulticospan.left I)]

Premises used: CategoryTheory.Limits.WalkingMulticospan.left
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
h :
  Eq (α := E.pt ⟶ P.obj (op I.Y)) (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op)
    (E.π.app (WalkingMulticospan.left I))
⊢ Eq (α := E.pt ⟶ P.obj (op I.Y))
    (E.π.app (WalkingMulticospan.left I) :
      Functor.obj (C := WalkingMulticospan S.shape) (Functor.obj (Functor.const (WalkingMulticospan S.shape)) E.pt)
          (WalkingMulticospan.left I) ⟶
        (S.index P).multicospan.obj (WalkingMulticospan.left I))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
A' : Type u₂
inst_2 : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst_3 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ Eq (α := E.pt ⟶ P.obj (op I.Y)) (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op)
    (E.π.app (WalkingMulticospan.left I))

Tactic:
apply hP.amalgamate_map

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))

Tactic:
⟨fun hP X S => ⟨isLimitOfIsSheaf _ _ _ hP⟩, ?_⟩

Premises used: Nonempty.intro, CategoryTheory.Presheaf.isLimitOfIsSheaf, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
refine : (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) → IsSheaf J P
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))

Tactic:
refine ⟨fun hP X S => ⟨isLimitOfIsSheaf _ _ _ hP⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
obtain :
  ∀ (hh : IsLimit (T.multifork P)),
    ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
obtain ⟨hh⟩ := h _ T
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
h₁ :
  (fun (t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (hh.lift K) ∧
    ∀ (y : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)),
      (fun (t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = hh.lift K
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
use hh.lift K

Premises used: CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
h₁ :
  x.IsAmalgamation (R := S.arrows) (hh.lift K) ∧
    ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K
⊢ (fun (t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (hh.lift K) ∧
    ∀ (y : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)),
      (fun (t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = hh.lift K

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
h₁ : x.IsAmalgamation (R := S.arrows) (hh.lift K)
h₂ : ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K
⊢ x.IsAmalgamation (R := S.arrows) (hh.lift K) ∧
    ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op E)).map f.op) :
        (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj (op E)).obj (op X))) →
          (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj (op E)).obj (op Y)))
      (hh.lift K) =
    x f hf

Tactic:
apply hh.fac K (WalkingMulticospan.left ⟨Y, f, hf⟩)

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.Limits.WalkingMulticospan.left, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation (R := S.arrows) e
h₁ : ∀ (j : WalkingMulticospan T.shape), e ≫ (T.multifork P).π.app j = K.π.app j
⊢ e = hh.lift K

Tactic:
apply hh.uniq K

Premises used: CategoryTheory.Limits.IsLimit.uniq
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation (R := S.arrows) e
a : T.shape.L
⊢ Eq (α := K.pt ⟶ (T.index P).multicospan.obj (WalkingMulticospan.left a))
    (e ≫ (T.multifork P).π.app (WalkingMulticospan.left a)) (K.π.app (WalkingMulticospan.left a))

Tactic:
apply he
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation (R := S.arrows) e
b : T.shape.R
h₁ :
  (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
⊢ Eq (α := K.pt ⟶ (T.index P).multicospan.obj (WalkingMulticospan.right b))
    (e ≫ (T.multifork P).π.app (WalkingMulticospan.right b)) (K.π.app (WalkingMulticospan.right b))

Tactic:
rw [← K.w (WalkingMulticospan.Hom.fst b), ←
        (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.Cover.multifork, CategoryTheory.Limits.Cone.w, CategoryTheory.Limits.WalkingMulticospan.Hom.fst
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation (R := S.arrows) e
b : T.shape.R
h₁ :
  Eq (α := K.pt ⟶ (T.index P).multicospan.obj (WalkingMulticospan.left (T.shape.fst b)))
    (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b)))
    (K.π.app (WalkingMulticospan.left (T.shape.fst b)))
⊢ (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
x : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows
hx : x.Compatible (R := S.arrows)
T : J.Cover X := Subtype.mk (p := fun (S : Sieve.{v₁, u₁} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) S hS
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun (I : T.shape.L) ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation (R := S.arrows) e
b : T.shape.R
⊢ Eq (α := K.pt ⟶ (T.index P).multicospan.obj (WalkingMulticospan.left (T.shape.fst b)))
    (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b)))
    (K.π.app (WalkingMulticospan.left (T.shape.fst b)))

Tactic:
apply he