awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
a : Y ⟶ F.obj (P := Presheaf.IsSheaf J).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)
    a
have tauto : ∀ ⦃Y_1 : C⦄,
  Presieve.FamilyOfElements.IsAmalgamation (R := arrows ⊥) (fun ⦃Y_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦ False.elim sorry)
      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_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦ False.elim sorry) t)
            y →
          y = t) →
      ∀ (f : Y_1 ⟶ X) (h : arrows ⊥ f),
        Eq (α := (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map f.op) :
                (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op X))) →
                  (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y_1)))
              a :
            (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
          ((fun ⦃Y_2 : C⦄ (f : Y_2 ⟶ X) (a : arrows ⊥ f) ↦
                (False.elim sorry : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_2)))
              f h :
            (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1))
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ IsTerminal F
have refine : IsTerminal (Functor.obj (sheafToPresheaf J A) F)
Tactic: refine IsTerminal.isTerminalOfObj (sheafToPresheaf _ _) _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ IsTerminal (Functor.obj (sheafToPresheaf J A) F)
have refine : ∀ (X : Cᵒᵖ), Membership.mem (γ := Set (Sieve.{v₁, u₁} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) ⊥
Tactic: refine Functor.isTerminal fun X ↦ Sheaf.isTerminalOfBotCover _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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.right b))
    (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b))
    (E.π.app (WalkingMulticospan.right b))
have right : (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) sorry ≫ (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: rw [← E.w (WalkingMulticospan.Hom.fst b),
        ← (S.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ (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)
have right : Eq (α := E.pt ⟶ (S.index P).multicospan.obj (WalkingMulticospan.left (S.shape.fst b)))
  (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) sorry ≫ (S.multifork P).π.app (WalkingMulticospan.left (S.shape.fst b)))
  (E.π.app (WalkingMulticospan.left (S.shape.fst b)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ m = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯
have h : ∀ (I : S.Arrow), m ≫ P.map I.f.op = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) sorry ≫ P.map I.f.op
Tactic: apply hP.hom_ext S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ m ≫ P.map I.f.op = hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) ⋯ ≫ P.map I.f.op
have 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) sorry ≫ P.map I.f.op)
Tactic: erw [hm (WalkingMulticospan.left I)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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))
    (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)
have h : Eq (α := E.pt ⟶ P.obj (op I.Y)) (hP.amalgamate S (fun (x : S.Arrow) ↦ E.ι x) sorry ≫ P.map I.f.op)
  (E.π.app (WalkingMulticospan.left I))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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))
have refine : (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) → IsSheaf J P
Tactic: refine ⟨fun hP X S => ⟨isLimitOfIsSheaf _ _ _ hP⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t
have obtain : ∀ (hh : IsLimit (T.multifork P)),
  ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t
Tactic: obtain ⟨hh⟩ := h _ T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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 ⋯) ⋯
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X), x.IsAmalgamation (R := S.arrows) t
have 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
Tactic: use hh.lift K
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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 ⋯) ⋯
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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 ⋯) ⋯
⊢ x.IsAmalgamation (R := S.arrows) (hh.lift K) ∧
    ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K
have h₁ : x.IsAmalgamation (R := S.arrows) (hh.lift K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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)
⊢ x.IsAmalgamation (R := S.arrows) (hh.lift K) ∧
    ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K
have h₂ : ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation (R := S.arrows) y → y = hh.lift K
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ e = hh.lift K
have h₁ : ∀ (j : WalkingMulticospan T.shape), e ≫ (T.multifork P).π.app j = K.π.app j
Tactic: apply hh.uniq K
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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.right b))
    (e ≫ (T.multifork P).π.app (WalkingMulticospan.right b)) (K.π.app (WalkingMulticospan.right b))
have 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)
Tactic: rw [← K.w (WalkingMulticospan.Hom.fst b), ←
        (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ (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)
have 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)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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'
hP : IsSheaf J P
X : C
S : J.Cover X
⊢ IsLimit (S.multifork P)
have rw : (hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) →
  {X : C} → (S : J.Cover X) → IsLimit (S.multifork P)
Tactic: rw [Presheaf.isSheaf_iff_multifork] at hP
Cleared hypotheses: hP, X, S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
have rw : (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
  ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
Tactic: rw [isSheaf_iff_multifork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
have refine_1 : ∀ (X : C) (S : J.Cover X),
  Nonempty (IsLimit (S.multifork P)) → IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
Tactic: refine forall₂_congr fun X S => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
refine_1 :
  ∀ (X : C) (S : J.Cover X),
    Nonempty (IsLimit (S.multifork P)) → IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
have refine_2 : ∀ (X : C) (S : J.Cover X),
  IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))
Tactic: refine forall₂_congr fun X S => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
⊢ Nonempty (IsLimit (S.multifork P))
have refine_2 : (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt
Tactic: refine ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ?_ ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
refine_2 : (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt
⊢ Nonempty (IsLimit (S.multifork P))
have refine_2₁ : ∀ (j : WalkingMulticospan S.shape),
  (limit.cone (S.index P).multicospan).π.app j =
    Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app j
Tactic: refine ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ?_ ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
inst_2 : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (Y := multiequalizer (S.index P)) (S.toMultiequalizer P)
a : WalkingMulticospan S.shape
⊢ (limit.cone (S.index P).multicospan).π.app a =
    Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app a
have refine_2 : Iso.hom (Iso.symm (asIso (S.toMultiequalizer P))) ≫ (S.multifork P).π.app a =
  (limit.cone (S.index P).multicospan).π.app a
Tactic: symm