awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z_1 : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z_1
hR : Sieve.ofArrows T g ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z_1
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : Eq (α := Z ⟶ Z_1.left) (gi ≫ (fun (i : ι) ↦ Over.Hom.left (g i)) i) (gj ≫ (fun (i : ι) ↦ Over.Hom.left (g i)) j)
rw : gj ≫ (T j).hom = gi ≫ Over.Hom.left (g i) ≫ Z_1.hom
rw₁ : gj ≫ (T j).hom = gj ≫ Over.Hom.left (g j) ≫ Z_1.hom
rw₂ rw₃ : gj ≫ Over.Hom.left (g j) ≫ Z_1.hom = gj ≫ Over.Hom.left (g j) ≫ Z_1.hom
⊢ gj ≫ (T j).hom = gi ≫ (T i).hom

Tactic:
rw [← Over.w (g i), reassoc_of% hgij, ← Over.w (g j)]

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

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

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

Tactic:
exact hgij
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR : Sieve.ofArrows T g ∈ (J.over X : (a : Over X) → Set (Sieve a)) Z
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
rw :
  ∀
    (hR :
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
        (Sieve.generate
          (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
            Functor.map (Over.forget X) (g i))))
    (t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows)
    (ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)),
    ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
      t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1
⊢ ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
    t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1

Tactic:
rw [J.mem_over_iff, Sieve.ofArrows, Sieve.overEquiv_generate,
    ← Sieve.arrows_generate_map_eq_functorPushforward, Sieve.generate_sieve,
    Presieve.map_ofArrows] at hR

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Sieve.ofArrows, CategoryTheory.Presieve.map_ofArrows, CategoryTheory.Sieve.generate_sieve, CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward, CategoryTheory.Sieve.overEquiv_generate
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
obtain :
  ∀ (a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left))
    (ha :
      hg.familyOfElements.sieveExtend (R :=
            Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
        (R :=
        Sieve.arrows
          (Sieve.generate
            (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
              Functor.map (Over.forget X) (g i))))
        a)
    (huniq :
      ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
        (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
              hg.familyOfElements.sieveExtend (R :=
                    Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
                (R :=
                Sieve.arrows
                  (Sieve.generate
                    (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                      Functor.map (Over.forget X) (g i))))
                t_1)
            y →
          y = a),
    ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
      t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1
⊢ ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
    t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1

Tactic:
obtain ⟨a, ha, huniq⟩ := Subcanonical.isSheaf_of_isRepresentable
    (CategoryTheory.yoneda.obj E.left) _ hR _ hg.familyOfElements_compatible.sieveExtend

Premises used: CategoryTheory.yoneda, CategoryTheory.Over.left, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
⊢ ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
    t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1

Tactic:
⟨?_, ?_, fun y hty ↦ ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
refine_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)
refine_2 :
  (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)) ↦
      t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1)
    (Over.homMk a ⋯)
refine_3 :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z))
    (hty :
      (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)) ↦
          t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1)
        y),
    y = Over.homMk a ⋯
⊢ ∃! t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z),
    t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1

Tactic:
refine ⟨?_, ?_, fun y hty ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
refine_1 : a ≫ E.hom = (Opposite.unop (Opposite.op Z)).hom
⊢ Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)

Tactic:
refine Over.homMk a ?_

Premises used: CategoryTheory.Over.homMk
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
⊢ a ≫ E.hom = (Opposite.unop (Opposite.op Z)).hom

Tactic:
(Subcanonical.isSheaf_of_isRepresentable <| CategoryTheory.yoneda.obj X)
      (.ofArrows _ <| fun i ↦ (g i).left) hR |>.isSeparatedFor.ext ?_

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.yoneda, CategoryTheory.Sieve.ofArrows, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
W Y : C
i : ι
v : W ⟶ (T i).left
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (Functor.map (Functor.obj CategoryTheory.yoneda E.left)
              (Quiver.Hom.op (Functor.map (Over.forget X) (g i)))) :
          TypeCat.Fun (Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left))
            (Functor.obj (Functor.obj CategoryTheory.yoneda E.left)
              (Opposite.op (Functor.obj (Over.forget X) (T i))))) :
        (a : (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left))) →
          (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E.left).obj (Opposite.op ((Over.forget X).obj (T i)))))
      a =
    hg.familyOfElements.sieveExtend (R :=
      Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i))
      (Functor.map (Over.forget X) (g i)) ⋯

Tactic:
have := ha _ (Sieve.ofArrows_mk _ _ i)
-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
W Y : Over.{v_1, u_1} X
i : ι
v : W ⟶ T i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj CategoryTheory.yoneda E) (v ≫ g i).op) :
        (a : (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E).obj (Opposite.op Z))) →
          (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E).obj (Opposite.op W)))
      (Over.homMk a ⋯) =
    t (v ≫ g i) ⋯

Tactic:
Over.OverMorphism.ext ?_

Premises used: CategoryTheory.Over.OverMorphism.ext