awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
apply :
  ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄,
    (Sieve.coverByImage G Y).arrows f →
      Sieve.pullback f
          (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))) ∈
        (K : (a : D) → Set (Sieve a)) Y_1
⊢ Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))) ∈
    (K : (a : D) → Set (Sieve a)) Y

Tactic:
apply K.transitive (G.is_cover_of_isCoverDense _ _) _

Premises used: CategoryTheory.GrothendieckTopology.transitive, CategoryTheory.Functor.is_cover_of_isCoverDense
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
rw :
  Sieve.pullback iWZ
      (Sieve.pullback iZY
        (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))) ∈
    (K : (a : D) → Set (Sieve a)) W
⊢ Sieve.pullback (iWZ ≫ iZY)
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))) ∈
    (K : (a : D) → Set (Sieve a)) W

Tactic:
rw [Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
hS :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback iZY
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))))
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY
        (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))) ∈
    (K : (a : D) → Set (Sieve a)) W

Tactic:
apply K.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
apply :
  Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
    Sieve.pullback iZY
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback iZY
      (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X))))))

Tactic:
apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Functor.functorPushforward_imageSieve_mem, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.functorPullback G (↑T : Sieve (G.obj X))).arrows iVX

Tactic:
simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, Subtype.val
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ ((iWV ≫ G.map iVZ) ≫ iZY) ≫ iYX = iWV ≫ G.map iVX

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : C
T : (↑((K : (a : D) → Set (Sieve a)) (G.obj X)) : Type (max u_2 v_2))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T : Sieve (G.obj X)).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.pullback iZY
        (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G (↑T : Sieve (G.obj X)))))).arrows
    (iWV ≫ G.map iVZ)

Tactic:
exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
D : Type u_2
inst : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_1 : Category.{v_4, u_4} A
ℱ : Sheaf.{v_2, v_4, u_2, u_4} K A
X : A
U : D
T : Sieve.{v_2, u_2} U
hT : T ∈ (K : (a : D) → Set (Sieve a)) U
x : FamilyOfElements (ℱ.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op X)) T.arrows
hx : x.Compatible (R := T.arrows)
t : (ℱ.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op X)).obj (op U)
h : x.IsAmalgamation (R := T.arrows) t
⊢ t = ⋯.amalgamate (R := T.arrows) x hx

Tactic:
(ℱ.property X T hT).isSeparatedFor x t _ h ((ℱ.property X T hT).isAmalgamation hx)

Premises used: CategoryTheory.Presieve.IsSheafFor.isAmalgamation, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X_1 Y_1 : C
i_1 : G.obj X_1 ⟶ G.obj Y_1
x_1 : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y_1))
X Y : C
i : X ⟶ Y
x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map i).op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
            x :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
          (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (G.map i).op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
            x :
          (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))

Tactic:
ConcreteCategory.congr_hom (α.naturality i.op).symm x

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X_1 Y_1 : C
i_1 : G.obj X_1 ⟶ G.obj Y_1
x_1 : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y_1))
X Y : C
i : X ⟶ Y
x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map i).op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
            x :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
          (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (G.map i).op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
            x :
          (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))

Tactic:
exact ConcreteCategory.congr_hom (α.naturality i.op).symm x

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))
⊢ ∀ {X Y : C} (i : X ⟶ Y) (x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map i).op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
              x :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
            (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (G.map i).op) :
                (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
              x :
            (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
        (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))

Tactic:
have {X Y} (i : X ⟶ Y) (x) :
      ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
    exact ConcreteCategory.congr_hom (α.naturality i.op).symm x
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map i).op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
              x :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
            (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (G.map i).op) :
                (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
              x :
            (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
        (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map i.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
            x :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
          (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
            x :
          (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))

Tactic:
IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_

Premises used: CategoryTheory.Functor.IsLocallyFull.ext
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
h :
  ∀ (x : (G.op ⋙ ℱ).obj (op Y)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op ≫ α.app (op X))).toFun x
⊢ α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op = ℱ.map i.op ≫ α.app (op X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op ≫ α.app (op X))).toFun x

Tactic:
naturality_apply α i _

Premises used: CategoryTheory.Functor.IsCoverDense.Types.naturality_apply
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map i.op)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op ≫ α.app (op X))).toFun x

Tactic:
exact naturality_apply α i _

Premises used: CategoryTheory.Functor.IsCoverDense.Types.naturality_apply
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
x : ℱ.obj (op X)
⊢ pushforwardFamily α x = fun (x_1 : D) (x_2 : x_1 ⟶ X) (hf : coverByImage G X x_2) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op) :
        (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (G.op.obj (op (Nonempty.some hf).1)))) →
          (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op x_1)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op (Nonempty.some hf).1)) :
            (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op (Nonempty.some hf).1))) →
              (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op (Nonempty.some hf).1)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (Nonempty.some hf).map.op) :
                (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) →
                  (fun (X : Type v) ↦ X) (ℱ.obj (G.op.obj (op (Nonempty.some hf).1))))
              x :
            (fun (X : Type v) ↦ X) (ℱ.obj (G.op.obj (op (Nonempty.some hf).1)))) :
        (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op (Nonempty.some hf).1)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily, rfl
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
simp :
  Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some ⋯).lift.op) :
          (a : ℱ'.obj.obj (op (G.obj (Nonempty.some ⋯).1))) → ℱ'.obj.obj (op (G.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op (Nonempty.some ⋯).1)) :
              (a : (G.op ⋙ ℱ).obj (op (Nonempty.some ⋯).1)) → (G.op ⋙ ℱ'.obj).obj (op (Nonempty.some ⋯).1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (Nonempty.some ⋯).map.op) :
                  (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj (Nonempty.some ⋯).1)))
                x :
              ℱ.obj (op (G.obj (Nonempty.some ⋯).1))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op (Nonempty.some ⋯).1)) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
          (a : (G.op ⋙ ℱ).obj (op Y)) → (G.op ⋙ ℱ'.obj).obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj Y))) x :
          ℱ.obj (op (G.obj Y))) :
      (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))
⊢ pushforwardFamily α x f ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
        (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y))))
          x :
        (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y))))

Tactic:
simp only [pushforwardFamily_def, op_obj]

Premises used: CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def, CategoryTheory.Functor.op_obj