awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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)
⊢ G.op.whiskerLeft (sheafHom α) = α
have w : ∀ (X : Cᵒᵖ), (G.op.whiskerLeft (sheafHom α)).app X = α.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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ᵒᵖ
⊢ (G.op.whiskerLeft (sheafHom α)).app X = α.app X
have w : Eq (α :=
  Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda ((G.op ⋙ ℱ).obj X))
    (obj yoneda ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj X)))
  (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) (map yoneda (α.app X))
Tactic: apply yoneda.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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ᵒᵖ
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda ((G.op ⋙ ℱ).obj X))
      (obj yoneda ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj X)))
    (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) (map yoneda (α.app X))
have w : ∀ (U : Aᵒᵖ) (x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) U))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x
Tactic: ext U
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) U))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x
have 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 (preimage yoneda ((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: dsimp [sheafHom, -yoneda_obj_obj, -yoneda_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ 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 (preimage yoneda ((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)
have w : 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: rw [yoneda.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ 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)
have 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)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ 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)
have w : (pushforwardFamily (homOver α (unop U)) x).Compatible (R := Sieve.arrows (Sieve.coverByImage G (G.obj (unop X))))
Tactic: apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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))))
⊢ 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)
have 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)
Tactic: apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
| ((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)))
have 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)))
Tactic: rw [← hf.some.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ (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
have 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
Tactic: conv_lhs => rw [← hf.some.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ (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
have 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
Tactic: simp only [Functor.map_comp, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ ((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
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ (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)
have 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)
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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)
⊢ sheafHom (G.op.whiskerLeft α) = α
have w : ∀ (X : Dᵒᵖ), (sheafHom (G.op.whiskerLeft α)).app X = α.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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ᵒᵖ
⊢ (sheafHom (G.op.whiskerLeft α)).app X = α.app X
have 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))
Tactic: apply yoneda.map_injective