awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
refine_1 :
  ∀ (t : P.obj (op B)) (ht₁ : hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t)
    (ht₂ :
      ∀ (y : P.obj (op B)),
        (fun (t : P.obj (op B)) ↦ hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t) y → y = t),
    ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x i
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := h _ hx.familyOfElements_compatible

Premises used: CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t
ht₂ :
  ∀ (y : P.obj (op B)), (fun (t : P.obj (op B)) ↦ hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t) y → y = t
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i

Tactic:
⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements, Eq, DFunLike.coe, _private.0.CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows.match_1
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t
ht₂ :
  ∀ (y : P.obj (op B)), (fun (t : P.obj (op B)) ↦ hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t) y → y = t
refine_1 :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        t =
      x i
refine_1₁ :
  ∀ (t' : (fun (X : Type w) ↦ X) (P.obj (op B)))
    (ht' :
      (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i)
        t')
    (x_1 : C) (x_2 : x_1 ⟶ B),
    ofArrows X π x_2 →
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t' =
          hx.familyOfElements (π i) ⋯
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i

Tactic:
refine ⟨t, fun i ↦ ?_, fun t' ht' ↦ ht₂ _ fun _ _ ⟨i⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t
ht₂ :
  ∀ (y : P.obj (op B)), (fun (t : P.obj (op B)) ↦ hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t) y → y = t
i : I
refine_1 : hx.familyOfElements (π i) ⋯ = x i
refine_1₁ refine_1₂ : x i = x i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      t =
    x i

Tactic:
rw [ht₁ _ (ofArrows.mk i), hx.familyOfElements_ofArrows_mk]

Premises used: CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_ofArrows_mk, CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t
ht₂ :
  ∀ (y : P.obj (op B)), (fun (t : P.obj (op B)) ↦ hx.familyOfElements.IsAmalgamation (R := ofArrows X π) t) y → y = t
t' : (fun (X : Type w) ↦ X) (P.obj (op B))
ht' :
  (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x i)
    t'
x_1 : C
x_2 : x_1 ⟶ B
h_1 : ofArrows X π x_2
i : I
refine_1 : x i = hx.familyOfElements (π i) ⋯
refine_1₁ refine_1₂ : x i = x i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
      t' =
    hx.familyOfElements (π i) ⋯

Tactic:
rw [ht', hx.familyOfElements_ofArrows_mk]

Premises used: CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_ofArrows_mk
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible (R := ofArrows X π)
refine_2 :
  ∀ (t : P.obj (op B))
    (hA :
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x (π i) ⋯)
    (ht :
      ∀ (y : (fun (X : Type w) ↦ X) (P.obj (op B))),
        (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
              ∀ (i : I),
                (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                      (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                    t =
                  x (π i) ⋯)
            y →
          y = t),
    ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t
⊢ ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t

Tactic:
obtain ⟨t, hA, ht⟩ := h (fun i ↦ x (π i) (ofArrows.mk _))
      (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible (R := ofArrows X π)
t : P.obj (op B)
hA :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        t =
      x (π i) ⋯
ht :
  ∀ (y : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x (π i) ⋯)
        y →
      y = t
⊢ ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t

Tactic:
⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, ExistsUnique, And.intro, Exists.intro, Eq, DFunLike.coe, _private.0.CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows.match_1
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible (R := ofArrows X π)
t : P.obj (op B)
hA :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        t =
      x (π i) ⋯
ht :
  ∀ (y : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x (π i) ⋯)
        y →
      y = t
⊢ ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t

Tactic:
exact ⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X_1 Y : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
s : P.obj (op B)
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
h : gi ≫ π i = gj ≫ π j
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gi.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                s :
              (fun (X : Type w) ↦ X) (P.obj (op (X i)))))
          i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                s :
              (fun (X : Type w) ↦ X) (P.obj (op (X i)))))
          j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
simp [← comp_apply, ← Functor.map_comp, ← op_comp, h]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
rw :
  (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    Function.Bijective (Arrows.toCompatible P π)
⊢ IsSheafFor P (ofArrows X π) ↔ Function.Bijective (Arrows.toCompatible P π)

Tactic:
rw [isSheafFor_arrows_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_arrows_iff
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    Function.Bijective (Arrows.toCompatible P π)

Tactic:
⟨fun h ↦ ⟨fun x₁ x₂ hx ↦
      (h _ (Arrows.toCompatible P π x₁).property).unique (fun _ ↦ rfl)
        (congr_fun (congr_arg Subtype.val hx.symm)),
      fun ⟨y, hy⟩ ↦ ?_⟩, fun h x hx ↦ ?_⟩

Premises used: Exists, CategoryTheory.Presieve.Arrows.toCompatible, congr_arg, _private.0.CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible.match_1, And.intro, Iff.intro, ExistsUnique.unique, congr_fun, Eq.symm, Subtype.val, Eq, rfl, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
refine_1 :
  ∀
    (h :
      ∀ (x : (i : I) → P.obj (op (X i))),
        Arrows.Compatible P π x →
          ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
            ∀ (i : I),
              (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                  t =
                x i)
    (x : Subtype (Arrows.Compatible P π)) (y : (i : I) → P.obj (op (X i))) (hy : Arrows.Compatible P π y),
    ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
refine_2 :
  ∀ (h : Function.Bijective (Arrows.toCompatible P π)) (x : (i : I) → P.obj (op (X i))) (hx : Arrows.Compatible P π x),
    ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x i
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i) ↔
    Function.Bijective (Arrows.toCompatible P π)

Tactic:
refine ⟨fun h ↦ ⟨fun x₁ x₂ hx ↦
      (h _ (Arrows.toCompatible P π x₁).property).unique (fun _ ↦ rfl)
        (congr_fun (congr_arg Subtype.val hx.symm)),
      fun ⟨y, hy⟩ ↦ ?_⟩, fun h x hx ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
refine_1 :
  ∀ (x : P.obj (op B))
    (hx :
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            x =
          y i),
    (∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
        (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
              ∀ (i : I),
                (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                      (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                    t =
                  y i)
            y_1 →
          y_1 = x) →
      ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy
⊢ ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy

Tactic:
obtain ⟨x, hx, _⟩ := h y hy
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x_1 : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        x =
      y i
right :
  ∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              y i)
        y_1 →
      y_1 = x
a :
  ∀ (x_2 : I),
    (↑(Arrows.toCompatible P π x) : (i : I) → P.obj (op (X i))) x_2 =
      (↑(Subtype.mk (p := Arrows.Compatible P π) y hy) : (i : I) → P.obj (op (X i))) x_2
⊢ Arrows.toCompatible P π x = Subtype.mk (p := Arrows.Compatible P π) y hy

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x_1 : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        x =
      y i
right :
  ∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              y i)
        y_1 →
      y_1 = x
x_2 : I
⊢ (↑(Arrows.toCompatible P π x) : (i : I) → P.obj (op (X i))) x_2 =
    (↑(Subtype.mk (p := Arrows.Compatible P π) y hy) : (i : I) → P.obj (op (X i))) x_2

Tactic:
apply hx
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
              t =
            x i
x_1 : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx :
  ∀ (i : I),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
        x =
      y i
right :
  ∀ (y_1 : (fun (X : Type w) ↦ X) (P.obj (op B))),
    (fun (t : (fun (X : Type w) ↦ X) (P.obj (op B))) ↦
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              y i)
        y_1 →
      y_1 = x
⊢ ∃ (a : P.obj (op B)), Arrows.toCompatible P π a = Subtype.mk (p := Arrows.Compatible P π) y hy

Tactic:
exact ⟨x, by ext; apply hx⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
refine_2 :
  ∀ (y : P.obj (op B)) (hy : Arrows.toCompatible P π y = Subtype.mk (p := Arrows.Compatible P π) x hx),
    ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x i
⊢ ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x i

Tactic:
obtain ⟨y, hy⟩ := h.2 ⟨x, hx⟩

Premises used: Subtype.mk, And.right
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : Arrows.toCompatible P π y = Subtype.mk (p := Arrows.Compatible P π) x hx
⊢ (↑(Arrows.toCompatible P π y) : (i : I) → P.obj (op (X i))) =
    (↑(Subtype.mk (p := Arrows.Compatible P π) x hx) : (i : I) → P.obj (op (X i)))

Tactic:
rw [Subtype.ext_iff] at hy

Premises used: Subtype.ext_iff