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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
w :
  Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
⊢ Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) 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
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
w :
  Eq (α := (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x;
    this)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
⊢ Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)

Tactic:
change (show (ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))) from _) = _
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
w : (pushforwardFamily (homOver α (unop U)) x).Compatible (R := Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))))
w₁ :
  (pushforwardFamily (homOver α (unop U)) x).IsAmalgamation (R := Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x;
    this)
⊢ Eq (α := (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x;
    this)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)

Tactic:
apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)

Premises used: CategoryTheory.Functor.is_cover_of_isCoverDense, 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
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
⊢ (pushforwardFamily (homOver α (unop U)) x).Compatible (R := Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))))

Tactic:
(pushforwardFamily_compatible _ _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, CategoryTheory.Presieve.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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
⊢ (pushforwardFamily (homOver α (unop U)) x).Compatible (R := Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))))

Tactic:
exact (pushforwardFamily_compatible _ _)

Premises used: CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).map
            ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op Y)))
      (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
            (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
              (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
          x;
      this) :
    (fun (X : Type v_4) ↦ X) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op Y)))
| ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).map f.op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op Y)))
      (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
            (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
              (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
          x;
      this) :
    (fun (X : Type v_4) ↦ X) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op Y)))

Tactic:
rw [← hf.some.fac]

Premises used: CategoryTheory.Presieve.CoverByImageStructure.fac, Nonempty.some
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).map
            ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op Y)))
      (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
            (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
              (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
          x;
      this) =
    pushforwardFamily (homOver α (unop U)) x f hf
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).map f.op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op Y)))
      (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
            (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
              (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
          x;
      this) =
    pushforwardFamily (homOver α (unop U)) x f hf

Tactic:
conv_lhs => rw [← hf.some.fac]

Premises used: CategoryTheory.Presieve.CoverByImageStructure.fac, Nonempty.some
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  (x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).map
            ((Nonempty.some hf).lift ≫ (Nonempty.some hf).map).op) :
        (a : (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (unop X))))) →
          (fun (X : Type v_4) ↦ X) ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op Y)))
      (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (G.obj (unop X))) :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
            (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
              (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
          x;
      this) =
    pushforwardFamily (homOver α (unop U)) x f hf

Tactic:
dsimp
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  ((x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op
⊢ (x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op

Tactic:
simp only [Functor.map_comp, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  (x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    (x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)
⊢ ((x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op

Tactic:
congr 1
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  x ≫ α.app X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    x ≫ ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
⊢ (x ≫ α.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    (x ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)

Tactic:
simp only [Category.assoc]

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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
w :
  α.app X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
⊢ x ≫ α.app X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    x ≫ ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Tactic:
congr 1
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
Y : D
f : Y ⟶ G.obj (unop X)
hf : Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))) f
⊢ α.app X ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).map.op =
    ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)

Tactic:
simpa using naturality_apply (G := G) (ℱ := ℱ ⋙ coyoneda.obj (op <| (G.op ⋙ ℱ).obj X))
    (ℱ' := ⟨_, Presheaf.isSheaf_comp_of_isSheaf K ℱ'.obj
      (coyoneda.obj (op ((G.op ⋙ ℱ).obj X))) ℱ'.property⟩)
    (whiskerRight α (coyoneda.obj _)) hf.some.map (𝟙 _)

Premises used: CategoryTheory.coyoneda, CategoryTheory.CategoryStruct.id, Nonempty.some, CategoryTheory.Presieve.CoverByImageStructure.map, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.IsCoverDense.Types.naturality_apply, CategoryTheory.Functor.obj
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
w : ∀ (X : Dᵒᵖ), (sheafHom (G.op.whiskerLeft α)).app X = α.app X
⊢ sheafHom (G.op.whiskerLeft α) = α

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
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
w :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda (ℱ.obj X))
      (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)))
    (map yoneda ((sheafHom (G.op.whiskerLeft α)).app X)) (map yoneda (α.app X))
⊢ (sheafHom (G.op.whiskerLeft α)).app X = α.app X

Tactic:
apply yoneda.map_injective

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_injective
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
w :
  ∀ (U : Aᵒᵖ) (x : obj (obj yoneda (ℱ.obj X)) U),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((sheafHom (G.op.whiskerLeft α)).app X)) U))
        x =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda (ℱ.obj X))
      (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)))
    (map yoneda ((sheafHom (G.op.whiskerLeft α)).app X)) (map yoneda (α.app X))

Tactic:
ext U
-- 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
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
w :
  Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (map yoneda (preimage yoneda ((sheafYonedaHom (G.op.whiskerLeft α)).app X))) U) :
          (a : (yoneda.obj (ℱ.obj X)).obj U) → (yoneda.obj (ℱ'.obj.obj X)).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj X)).obj U) → (yoneda.obj (ℱ'.obj.obj X)).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)) U)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((sheafHom (G.op.whiskerLeft α)).app X)) U))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x

Tactic:
dsimp [sheafHom, -yoneda_obj_obj, -yoneda_map_app]

Premises used: CategoryTheory.yoneda_map_app, CategoryTheory.Functor.IsCoverDense.sheafHom, CategoryTheory.yoneda_obj_obj