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
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ Subsingleton.{v₂ + 1} ({ pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op)
have mpr : ∀ (a b : { pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op), a = b
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
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := π : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op), a = b
have mpr : ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op),
  a = b
Tactic: rw [← eqv.left_inv π]
-- 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
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasPullbacks.{v₁, u₁} C
K : Pretopology.{v₁, u₁} C
⊢ (∀ (E : A), Presieve.IsSheaf.{v₂, v₁, u₁} K.toGrothendieck (P ⋙ Functor.obj coyoneda (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
have simp_rw : (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ Functor.obj coyoneda (op E)) R) ↔
  ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
Tactic: simp_rw [isSheaf_pretopology]
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ x = y
have h₁ : ∀
  (I_1 :
    GrothendieckTopology.Cover.Arrow
      (Subtype.mk (p := fun (S_1 : Sieve.{v₁, u₁} S) ↦ S_1 ∈ (J : (a : C) → Set (Sieve a)) S) (ofArrows X f) hf)),
  x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op
Tactic: apply hP.hom_ext ⟨_, hf⟩
-- 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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ Eq (α :=
    E ⟶
      P.obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S_1 : Sieve.{v₁, u₁} S) ↦ S_1 ∈ (J : (a : C) → Set (Sieve a)) S) (ofArrows X f) hf)
            { Y := Z, f := g ≫ f i, hf := ⋯ })))
    (x ≫ P.map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z, f := g ≫ f i, hf := ⋯ })))
    (y ≫ P.map (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := Z, f := g ≫ f i, hf := ⋯ })))
have h₁ : Eq (α := E ⟶ P.obj (op Z)) (x ≫ P.map ((f i).op ≫ g.op)) (y ≫ P.map ((f i).op ≫ g.op))
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
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ Eq (α := E ⟶ P.obj (op Z)) (x ≫ P.map ((f i).op ≫ g.op)) (y ≫ P.map ((f i).op ≫ g.op))
have h₁ : x ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op
Tactic: rw [P.map_comp, reassoc_of% (h 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
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ (J : (a : C) → Set (Sieve a)) S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
h₁ : x ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op
⊢ Eq (α := E ⟶ P.obj (op Z)) (x ≫ P.map ((f i).op ≫ g.op)) (y ≫ P.map ((f i).op ≫ g.op))
have h₂ : y ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op
Tactic: rw [P.map_comp, reassoc_of% (h i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P
have mp : Presheaf.IsSheaf J P → Presieve.IsSheaf J P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
mp : Presheaf.IsSheaf J P → Presieve.IsSheaf J P
⊢ Presheaf.IsSheaf J P ↔ Presieve.IsSheaf J P
have mpr : Presieve.IsSheaf J P → Presheaf.IsSheaf J P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presheaf.IsSheaf J P
⊢ Presieve.IsSheaf J P
have mp : P ⋙ Functor.obj coyoneda (op PUnit.{w + 1}) ≅ P
Tactic: refine Presieve.isSheaf_iso J ?_ (hP (PUnit))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y), z.IsAmalgamation (R := S.arrows) t
have mpr : ∀ (x : unop (op X)),
  Presieve.FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := S.arrows) fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x
Tactic: refine ⟨↾fun x => (hP S hS).amalgamate (fun Z f hf ↦
      (ConcreteCategory.hom (z f hf)) x) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
mpr :
  ∀ (x : unop (op X)),
    Presieve.FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := S.arrows)
      fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y), z.IsAmalgamation (R := S.arrows) t
have mpr₁ : (fun (t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)) ↦ z.IsAmalgamation (R := S.arrows) t)
  (↾fun (x : unop (op X)) ↦
    sorry.amalgamate (R := S.arrows)
      (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
      sorry)
Tactic: refine ⟨↾fun x => (hP S hS).amalgamate (fun Z f hf ↦
      (ConcreteCategory.hom (z f hf)) x) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
mpr :
  ∀ (x : unop (op X)),
    Presieve.FamilyOfElements.Compatible.{w, v₁, u₁} (P := P) (R := S.arrows)
      fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x
mpr₁ :
  (fun (t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)) ↦ z.IsAmalgamation (R := S.arrows) t)
    (↾fun (x : unop (op X)) ↦
      ⋯.amalgamate (R := S.arrows)
        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
        ⋯)
⊢ ∃! t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y), z.IsAmalgamation (R := S.arrows) t
have mpr₂ : ∀ (y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)),
  (fun (t : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)) ↦ z.IsAmalgamation (R := S.arrows) t) y →
    y =
      ↾fun (x : unop (op X)) ↦
        sorry.amalgamate (R := S.arrows)
          (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
          sorry
Tactic: refine ⟨↾fun x => (hP S hS).amalgamate (fun Z f hf ↦
      (ConcreteCategory.hom (z f hf)) x) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
        (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
          (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
      (↾fun (x : unop (op X)) ↦
        ⋯.amalgamate (R := S.arrows)
          (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
          ⋯) =
    z f hf
have mpr : ∀ (x : unop (op X)),
  Eq (α := P.obj (op Z))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
                (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
                  (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
              (↾fun (x : unop (op X)) ↦
                sorry.amalgamate (R := S.arrows)
                  (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                  sorry)) :
          (a : unop (op X)) → P.obj (op Z))
        x :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z))
Tactic: apply ConcreteCategory.hom_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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
Z : C
f : Z ⟶ Y
hf : S.arrows f
x : unop (op X)
⊢ Eq (α := P.obj (op Z))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda (op X)).map f.op) :
                (a : (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Y))) →
                  (fun (X : Type w) ↦ X) ((P ⋙ coyoneda.obj (op X)).obj (op Z)))
              (↾fun (x : unop (op X)) ↦
                ⋯.amalgamate (R := S.arrows)
                  (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                  ⋯)) :
          (a : unop (op X)) → P.obj (op Z))
        x :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x : P.obj (op Z))
have mpr : Eq (α := P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) : (a : P.obj (op Y)) → P.obj (op Z))
      (sorry.amalgamate (R := S.arrows)
        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x)
        sorry) :
    P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : X) → P.obj (op Z)) x : P.obj (op Z))
Tactic: simp only [Functor.comp_obj, Functor.flip_obj_obj, yoneda_obj_obj, Functor.comp_map,
        Functor.flip_obj_map, yoneda_map_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)
hy : z.IsAmalgamation (R := S.arrows) y
⊢ y =
    ↾fun (x : unop (op X)) ↦
      ⋯.amalgamate (R := S.arrows)
        (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
        ⋯
have mpr : ∀ (x : unop (op X)),
  Eq (α := P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : unop (op X)) ↦
              sorry.amalgamate (R := S.arrows)
                (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                sorry) :
          (a : unop (op X)) → P.obj (op Y))
        x :
      P.obj (op Y))
Tactic: apply ConcreteCategory.hom_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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve.{v₁, u₁} Y
hS : S ∈ (J : (a : C) → Set (Sieve a)) Y
z : Presieve.FamilyOfElements (P ⋙ Functor.obj coyoneda (op X)) S.arrows
hz : z.Compatible (R := S.arrows)
y : (P ⋙ Functor.obj coyoneda (op X)).obj (op Y)
hy : z.IsAmalgamation (R := S.arrows) y
x : unop (op X)
⊢ Eq (α := P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : unop (op X)) ↦
              ⋯.amalgamate (R := S.arrows)
                (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                ⋯) :
          (a : unop (op X)) → P.obj (op Y))
        x :
      P.obj (op Y))
have mpr : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
  S.arrows f →
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) y : (a : unop (op X)) → P.obj (op Y)) x : P.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (↾fun (x : unop (op X)) ↦
                    sorry.amalgamate (R := S.arrows)
                      (fun (Z : C) (f : Z ⟶ Y) (hf : S.arrows f) ↦
                        (ConcreteCategory.hom (FC := TypeCat.Fun) (z f hf) : (a : unop (op X)) → P.obj (op Z)) x)
                      sorry) :
                (a : unop (op X)) → P.obj (op Y))
              x :
            P.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P.obj (op Y_1)))
Tactic: apply (hP S hS).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : GrothendieckTopology.{v₁, u₁} C
A_1 : Type u₂
inst_1 : Category.{v₂, u₂} A_1
A : Type u₂
inst_2 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
ℱ : Sheaf.{v₁, v₂, u₁, u₂} J A
E : A
⊢ Presheaf.IsSheaf J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))
have rw : Presieve.IsSheaf.{v₂, v₁, u₁} J (ℱ.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op E))
Tactic: rw [isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
hP : IsSheaf J P
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor P S.arrows
have rw : ∀ (hP : Presieve.IsSheaf J P) {X : C} (S : Sieve.{v₁, u₁} X) (hS : S ∈ (J : (a : C) → Set (Sieve a)) X),
  Presieve.IsSheafFor P S.arrows
Tactic: rw [isSheaf_iff_isSheaf_of_type] at hP
Cleared hypotheses: hP, X, S, hS
-- 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
⊢ IsTerminal.{v₂, u₂} (F.obj (P := Presheaf.IsSheaf J).obj (op X))
have refine : (X_1 : A) → Unique (X_1 ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
Tactic: refine @IsTerminal.ofUnique _ _ _ ?_
-- 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
⊢ Presieve.FamilyOfElements (X := X) (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)) (arrows ⊥)
have tauto : ⦃Y_1 : C⦄ → (f : Y_1 ⟶ X) → arrows ⊥ f → (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)
Tactic: tauto
-- 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
⊢ Presieve.FamilyOfElements.Compatible.{v₂, v₁, u₁} (P := F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y))
    (R := arrows ⊥) fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦ False.elim ⋯
have tauto : ∀ ⦃Y₁ Y₂ Z : C⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : arrows ⊥ f₁) (h₂ : arrows ⊥ f₂),
  g₁ ≫ f₁ = g₂ ≫ f₂ →
    Eq (α := (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map g₁.op) :
            (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y₁))) →
              (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Z)))
          ((fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦
              (False.elim sorry : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
            f₁ h₁) :
        (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).map g₂.op) :
            (a : (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Y₂))) →
              (fun (X : Type v₂) ↦ X) ((F.obj ⋙ coyoneda.obj (op Y)).obj (op Z)))
          ((fun ⦃Y_1 : C⦄ (f : Y_1 ⟶ X) (a : arrows ⊥ f) ↦
              (False.elim sorry : (F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Y_1)))
            f₂ h₂) :
        (fun (X : Type v₂) ↦ X) ((F.obj (P := Presheaf.IsSheaf J) ⋙ Functor.obj coyoneda (op Y)).obj (op Z)))
Tactic: tauto
-- 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
⊢ Unique (Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
have choose : (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 sorry) 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 sorry) t)
              y →
            y = t) →
    Unique (Y ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
Tactic: choose t h using F.2 Y _ H (by tauto) (by tauto)