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
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.inv X ≫ appHom i.hom 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.inv X ≫ appHom i.hom 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.inv X ≫ appHom i.hom 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
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : ℱ.obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun x
⊢ ℱ.map f ≫ appHom α (unop Y) = appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f

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
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
h :
  ∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ unop Y),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f_1.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y_1))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f_1.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (unop Y)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y_1))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun
            x) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y_1))))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).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
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
h :
  Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
          (a : ℱ'.obj.obj (op (unop Y))) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop Y)) : (a : ℱ.obj Y) → ℱ'.obj.obj Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj Y) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (f ≫ f'.op)) :
          (a : ℱ'.obj.obj X) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X)) : (a : ℱ.obj X) → ℱ'.obj.obj X) x :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj X) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
⊢ 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 (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y'))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f ≫ appHom α (unop Y))).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 (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y'))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f)).toFun
          x) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y'))))

Tactic:
simp only [TypeCat.Fun.toFun_apply, types_comp_apply, ← map_comp_apply]

Premises used: CategoryTheory.Functor.map_comp_apply, TypeCat.Fun.toFun_apply, CategoryTheory.types_comp_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
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
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
h :
  Eq (α := ℱ'.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'.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y'))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
          (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')))
    ((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 ≫ f'.op)) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop 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')))
⊢ Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op) :
          (a : ℱ'.obj.obj (op (unop Y))) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop Y)) : (a : ℱ.obj Y) → ℱ'.obj.obj Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj Y) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (f ≫ f'.op)) :
          (a : ℱ'.obj.obj X) → ℱ'.obj.obj (op (G.obj Y')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom α (unop X)) : (a : ℱ.obj X) → ℱ'.obj.obj X) x :
          ℱ'.obj (P := Presheaf.IsSheaf K).obj X) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y')))

Tactic:
rw [appHom_restrict, 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
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α_1 : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ Eq (α := ℱ'.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'.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y'))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map f) : (a : ℱ.obj X) → ℱ.obj Y) x : ℱ.obj Y) :
          (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')))
    ((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 ≫ f'.op)) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (unop 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:
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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
w :
  ∀ (U : Dᵒᵖ) (x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y))).app
              U)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((presheafHom (homOver α (unop X)) ≫
                  (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f).app
              U)).toFun
        x
⊢ (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y)) =
    presheafHom (homOver α (unop X)) ≫
      (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f

Tactic:
ext U 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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
w :
  Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
        (f.unop ≫ x) :
      (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
              (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
          x :
      unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (unop U)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).map f ≫ presheafHom (homOver α (unop Y))).app U)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((presheafHom (homOver α (unop X)) ≫
                (coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) (ℱ'.obj (P := Presheaf.IsSheaf K))).map f).app
            U)).toFun
      x

Tactic:
change
      appHom (homOver α (unop Y)) (unop U) (f.unop ≫ x) =
        f.unop ≫ appHom (homOver α (unop X)) (unop U) x

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.unop, CategoryTheory.Functor.IsCoverDense.Types.appHom, CategoryTheory.CategoryStruct.comp, DFunLike.coe, Opposite.unop, CategoryTheory.Functor.IsCoverDense.homOver
-- 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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
w :
  Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x))
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
        (f.unop ≫ x) :
      (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
              (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
          x :
      unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (unop U)))

Tactic:
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
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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
w :
  Membership.mem (γ := Set (Sieve.{v_2, u_2} (unop U))) ((K : (a : D) → Set (Sieve a)) (unop U))
    (Sieve.coverByImage G (unop U))
w₁ :
  (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible (R := Sieve.arrows (Sieve.coverByImage G (unop U)))
w₂ :
  (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation (R :=
    Sieve.arrows (Sieve.coverByImage G (unop U)))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
⊢ Eq (α := (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj (P := Presheaf.IsSheaf K).obj (op (unop U))))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop X))).obj (op (unop U)))) →
            (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop X)).obj.obj (op (unop U))))
        x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop Y)) (unop U)) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ ⋙ coyoneda.obj (op (unop Y))).obj (op (unop U)))) →
          (fun (X : Type v_4) ↦ X) ((sheafOver ℱ' (unop Y)).obj.obj (op (unop U))))
      (f.unop ≫ x))

Tactic:
apply sheaf_eq_amalgamation

Premises used: CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation
-- 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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (unop U))) ((K : (a : D) → Set (Sieve a)) (unop U))
    (Sieve.coverByImage G (unop U))

Tactic:
apply G.is_cover_of_isCoverDense

Premises used: 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
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
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible (R := Sieve.arrows (Sieve.coverByImage G (unop U)))

Tactic:
pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)

Premises used: CategoryTheory.Functor.comp, Quiver.Hom.unop, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, CategoryTheory.CategoryStruct.comp, CategoryTheory.Presieve.coverByImage, Opposite.unop, CategoryTheory.Functor.IsCoverDense.homOver