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 : 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
refine_2 :
  Over.Hom.left
      ((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 ⋯)) =
    Over.Hom.left (t (v ≫ g 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:
refine Over.OverMorphism.ext ?_

Premises used: CategoryTheory.Over.OverMorphism.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 : 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.left) (Over.Hom.left (g i)).op) :
        (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 (T i).left)))
      a =
    hg.familyOfElements.sieveExtend (R :=
      Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)) (Over.Hom.left (g i)) ⋯

Tactic:
have := ha (g i).left (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
this :
  Over.Hom.left (g i) ≫ a =
    hg.familyOfElements.sieveExtend (R :=
      Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)) (Over.Hom.left (g i)) ⋯
⊢ Over.Hom.left
      ((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 ⋯)) =
    Over.Hom.left (t (v ≫ g i) ⋯)

Tactic:
simp [Category.assoc, this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i),
      Presieve.FamilyOfElements.comp_of_compatible _ ht (Sieve.ofArrows_mk _ _ i)]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Presieve.extend_agrees, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible, CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible
-- 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
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 ⋯

Tactic:
Over.OverMorphism.ext (huniq _ ?_)

Premises used: CategoryTheory.Over.OverMorphism.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 : 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
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
refine_3 :
  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))))
    (Over.Hom.left y)
⊢ y = Over.homMk a ⋯

Tactic:
refine Over.OverMorphism.ext (huniq _ ?_)

Premises used: CategoryTheory.Over.OverMorphism.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 : 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
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
W Y : C
i : ι
v : W ⟶ Functor.obj (Over.forget X) (T i)
⊢ Over.Hom.left
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj CategoryTheory.yoneda E) (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 (T i))))
        y) =
    Over.Hom.left (t (g i) ⋯)

Tactic:
have := congr($(hty _ (Sieve.ofArrows_mk _ _ i)).left)
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
J : GrothendieckTopology.{v, u} C
h : Presieve.IsSeparated J F
⊢ Presieve.IsSeparated.{w, v, u} J G.toFunctor

Tactic:
fun _ S hS _ _ _ hx₁ hx₂ ↦ Subtype.ext <| h S hS _ _ _ (hx₁.map G.ι) (hx₂.map G.ι)

Premises used: CategoryTheory.Presieve.IsSeparatedFor, CategoryTheory.Subfunctor.ι, CategoryTheory.Presieve.FamilyOfElements.map, CategoryTheory.Presieve.IsSeparated, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.map, Subtype.val, Subtype.ext
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs :
  Membership.mem (γ := Set (F.obj U))
    {s : F.obj U |
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)}
    s
⊢ Membership.mem (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      {s : F.obj V |
        Membership.mem (γ := Set (Sieve.{v, u} (unop V))) ((J : (a : C) → Set (Sieve a)) (unop V))
          (G.sieveOfSection s)})
    s

Tactic:
J.superset_covering ?_ (J.pullback_stable i.unop hs)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, Set.Mem, setOf, Quiver.Hom.unop, CategoryTheory.GrothendieckTopology.pullback_stable, Set.preimage
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs :
  Membership.mem (γ := Set (F.obj U))
    {s : F.obj U |
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)}
    s
refine :
  Sieve.pullback i.unop (G.sieveOfSection s) ≤
    G.sieveOfSection
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        s)
⊢ Membership.mem (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      {s : F.obj V |
        Membership.mem (γ := Set (Sieve.{v, u} (unop V))) ((J : (a : C) → Set (Sieve a)) (unop V))
          (G.sieveOfSection s)})
    s

Tactic:
refine J.superset_covering ?_ (J.pullback_stable i.unop hs)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, Quiver.Hom.unop, CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs :
  Membership.mem (γ := Set (F.obj U))
    {s : F.obj U |
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)}
    s
Y : C
_ :
  ∀ (f : Y ⟶ unop V),
    (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f →
      Sieve.arrows
        (G.sieveOfSection
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) :
              (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
            s))
        f
⊢ ∀ (f : Y ⟶ unop V),
    (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f →
      Sieve.arrows
        (G.sieveOfSection
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) :
              (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
            s))
        f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs :
  Membership.mem (γ := Set (F.obj U))
    {s : F.obj U |
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)}
    s
Y : C
f : Y ⟶ unop V
h : (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f
dsimp :
  Membership.mem (α := F.obj (op Y)) (γ := Set (F.obj (op Y))) (G.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj V) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) s : F.obj V) :
      F.obj (op Y))
⊢ Sieve.arrows
    (G.sieveOfSection
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        s))
    f

Tactic:
dsimp at h ⊢
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs :
  Membership.mem (γ := Set (F.obj U))
    {s : F.obj U |
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)}
    s
Y : C
f : Y ⟶ unop V
h :
  Membership.mem (α := F.obj (op Y)) (γ := Set (F.obj (op Y))) (G.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ f.op)) : (a : F.obj U) → F.obj (op Y)) s : F.obj (op Y))
rwa :
  Membership.mem (α := F.obj (op Y)) (γ := Set (F.obj (op Y))) (G.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i ≫ F.map f.op) : (a : F.obj U) → F.obj (op Y)) s : F.obj (op Y))
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (α := F.obj (op Y)) (γ := Set (F.obj (op Y))) (G.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ f.op)) : (a : F.obj U) → F.obj (op Y)) s : F.obj (op Y))
⊢ Membership.mem (α := F.obj (op Y)) (γ := Set (F.obj (op Y))) (G.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj V) → F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) s : F.obj V) :
      F.obj (op Y))

Tactic:
rwa [← comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) ⊤

Tactic:
J.top_mem U.unop

Premises used: CategoryTheory.GrothendieckTopology.top_mem, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
h : G.sieveOfSection s = ⊤
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s)

Tactic:
convert! J.top_mem U.unop

Premises used: CategoryTheory.GrothendieckTopology.top_mem, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
h : ⊤ ≤ G.sieveOfSection s
⊢ G.sieveOfSection s = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
V : C
i : V ⟶ unop U
⊢ (G.sieveOfSection s).arrows i

Tactic:
G.map i.op hs

Premises used: Set.Mem, Quiver.Hom.op, setOf, CategoryTheory.Subfunctor.map, Set.preimage
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
V : C
i : V ⟶ unop U
⊢ (G.sieveOfSection s).arrows i

Tactic:
exact G.map i.op hs

Premises used: Quiver.Hom.op, CategoryTheory.Subfunctor.map