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
ℱ : 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
generalize :
  ∀ (l : CoverByImageStructure G f),
    Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map l.lift.op) :
            (a : ℱ'.obj.obj (op (G.obj l.1))) → ℱ'.obj.obj (op (G.obj Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op l.1)) :
                (a : (G.op ⋙ ℱ).obj (op l.1)) → (G.op ⋙ ℱ'.obj).obj (op l.1))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map l.map.op) : (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj l.1)))
                  x :
                ℱ.obj (op (G.obj l.1))) :
            (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op l.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))
⊢ 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))

Tactic:
generalize Nonempty.some (Presieve.in_coverByImage G f) = l

Premises used: Nonempty.some, CategoryTheory.Presieve.in_coverByImage
-- 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 W : C
iYW : G.obj Y ⟶ G.obj W
iWX : G.obj W ⟶ X
⊢ Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (ℱ'.obj (P := Presheaf.IsSheaf K).map
              { obj := W, lift := iYW, map := iWX, fac := ⋯ : CoverByImageStructure G (iYW ≫ iWX) }.lift.op) :
          (a : ℱ'.obj.obj (op (G.obj { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1))) → ℱ'.obj.obj (op (G.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (α.app (op { obj := W, lift := iYW, map := iWX, fac := ⋯ : CoverByImageStructure G (iYW ≫ iWX) }.1)) :
              (a : (G.op ⋙ ℱ).obj (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1)) →
                (G.op ⋙ ℱ'.obj).obj (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (ℱ.map
                      { obj := W, lift := iYW, map := iWX, fac := ⋯ : CoverByImageStructure G (iYW ≫ iWX) }.map.op) :
                  (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1)))
                x :
              ℱ.obj (op (G.obj { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.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 (iYW ≫ iWX).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))

Tactic:
simp only [← op_comp, ← Functor.map_comp_apply, naturality_apply]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply, 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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
                  (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                      (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                    x :
                  (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
              (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
          (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
                  (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                      (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                    x :
                  (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
              (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
          (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
W₂ : C
iYW₂ : Y₂ ⟶ G.obj W₂
iWX₂ : G.obj W₂ ⟶ X
h₂ : coverByImage G X (iYW₂ ≫ iWX₂)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ iYW₂ ≫ iWX₂
⊢ (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ : CoverByImageStructure G (iYW₁ ≫ iWX₁) }.lift) ≫
      { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ : CoverByImageStructure G (iYW₁ ≫ iWX₁) }.map =
    (iZY₂ ≫ { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ : CoverByImageStructure G (iYW₂ ≫ iWX₂) }.lift) ≫
      { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.map

Tactic:
simpa only [Category.assoc] using e

Premises used: CategoryTheory.Category.assoc
-- 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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
suffices :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
                  (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                      (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                    x :
                  (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
              (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
          (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
                  (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                    (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                      (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                    x :
                  (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
              (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
          (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
⊢ (pushforwardFamily α x).Compatible (R := coverByImage G X)

Tactic:
suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
      (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
    rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
    simp only [pushforwardFamily, ← Functor.map_comp_apply, ← op_comp]
    generalize Nonempty.some h₁ = l₁
    generalize Nonempty.some h₂ = l₂
    obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
    obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
    exact this _ _ _ _ (by simpa only [Category.assoc] using 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
ℱ : 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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Z : D
W₁ W₂ : C
iWX₁ : G.obj W₁ ⟶ X
iWX₂ : G.obj W₂ ⟶ X
iZW₁ : Z ⟶ G.obj W₁
iZW₂ : Z ⟶ G.obj W₂
e : iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                  (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                x :
              (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                  (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                x :
              (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))

Tactic:
ext G _ _ fun V iVZ ↦ ?_

Premises used: CategoryTheory.Functor.IsCoverDense.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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
x : (fun (X : Type v) ↦ X) (ℱ.obj (op X))
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α X) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op X)))
            x :
          (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((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) :
              (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)))) :
      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y)))

Tactic:
(((isSheaf_iff_isSheaf_of_type _ _).1 ℱ'.property _ (G.is_cover_of_isCoverDense _ X)).valid_glue
      (pushforwardFamily_compatible α x) f.unop
          (Presieve.in_coverByImage G f.unop)).trans (pushforwardFamily_apply _ _ _)

Premises used: Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.property, Quiver.Hom.unop, CategoryTheory.Functor.is_cover_of_isCoverDense, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, CategoryTheory.Presieve.IsSheafFor.amalgamate, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp, Classical.choose, CategoryTheory.Presieve.IsSheafFor.valid_glue, CategoryTheory.Presieve.in_coverByImage, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply, Eq.trans
-- 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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
h :
  ∀ (x : ℱ.obj (op X)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ α.app (op Y))).toFun x
⊢ appHom α X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f = ℱ.map f ≫ α.app (op Y)

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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
x : ℱ.obj (op X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ α.app (op Y))).toFun x

Tactic:
apply appHom_restrict

Premises used: CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
h :
  ∀ (x : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
⊢ appHom i.hom X ≫ appHom i.inv X = 𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))

Tactic:
ext 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
x : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
h :
  ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x) :
        (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x) :
        (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x

Tactic:
apply Functor.IsCoverDense.ext G

Premises used: CategoryTheory.Functor.IsCoverDense.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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
x : ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.hom X ≫ appHom i.inv X)).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x) :
      (fun (X : Type v) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))

Tactic:
simp
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ_1 : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ'_1 : Sheaf K (Type v)
α : G.op ⋙ ℱ_1 ⟶ G.op ⋙ ℱ'_1.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : D
h :
  ∀ (x : ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom i.inv X ≫ appHom i.hom X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X)))).toFun x
⊢ appHom i.inv X ≫ appHom i.hom X = 𝟙 (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op X))

Tactic:
ext x