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
α : ℱ ⟶ ℱ'.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) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)
⊢ 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)

Tactic:
rw [yoneda.map_preimage]

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_preimage
-- 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 (α.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) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)
⊢ Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)

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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
w :
  Eq (α := (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (unop X)))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (unop X)) :=
      (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;
    this)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)
⊢ Eq (α := 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)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)

Tactic:
change (show (ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
w :
  (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x).Compatible (R :=
    Sieve.arrows (Sieve.coverByImage G (unop X)))
w₁ :
  (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x).IsAmalgamation (R :=
    Sieve.arrows (Sieve.coverByImage G (unop X)))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (unop X)) :=
      (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;
    this)
⊢ Eq (α := (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (unop X)))
    (have this : (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ obj coyoneda (op (unop U))).obj (op (unop X)) :=
      (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;
    this)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app 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)

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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
⊢ (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x).Compatible (R :=
    Sieve.arrows (Sieve.coverByImage G (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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
⊢ (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x).Compatible (R :=
    Sieve.arrows (Sieve.coverByImage G (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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (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 (unop X)) :=
        (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;
      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 (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 (unop X)) :=
        (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;
      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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (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 (unop X)) :=
        (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;
      this) =
    pushforwardFamily (homOver (G.op.whiskerLeft α) (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 (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 (unop X)) :=
        (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;
      this) =
    pushforwardFamily (homOver (G.op.whiskerLeft α) (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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (G.obj (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 (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 (unop X)) :=
        (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;
      this) =
    pushforwardFamily (homOver (G.op.whiskerLeft α) (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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (G.obj (Nonempty.some hf).1))) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf).lift.op

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
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
f : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
𝒢' : Sheaf.{v_2, v_4, u_2, u_4} K A
g : ℱ' ⟶ 𝒢'
⊢ Eq (α := G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ 𝒢'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj) (f ≫ g.hom) :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ ℱ'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) f ≫ G.op.whiskerLeft g.hom :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
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
f : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
𝒢' : Sheaf.{v_2, v_4, u_2, u_4} K A
g : ℱ' ⟶ 𝒢'
a :
  Eq (α := G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ 𝒢'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj) → ℱ ⟶ 𝒢'.obj) (f ≫ G.op.whiskerLeft g.hom)) :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ 𝒢'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) f ≫ g.hom) :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
⊢ Eq (α := ℱ ⟶ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj) → ℱ ⟶ 𝒢'.obj) (f ≫ G.op.whiskerLeft g.hom) :
      ℱ ⟶ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) f ≫ g.hom :
      ℱ ⟶ 𝒢'.obj (P := Presheaf.IsSheaf K))

Tactic:
apply (restrictHomEquivHom (G := G)).symm.injective

Premises used: Equiv.injective, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, Equiv.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
f : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
𝒢' : Sheaf.{v_2, v_4, u_2, u_4} K A
g : ℱ' ⟶ 𝒢'
⊢ Eq (α := G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ 𝒢'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj) → ℱ ⟶ 𝒢'.obj) (f ≫ G.op.whiskerLeft g.hom)) :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ 𝒢'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) f ≫ g.hom) :
      G.op ⋙ ℱ ⟶ G.op ⋙ 𝒢'.obj (P := Presheaf.IsSheaf K))

Tactic:
simpa only [Equiv.symm_apply_apply] using
    (restrictHomEquivHom_naturality_right_symm (G := G) (restrictHomEquivHom f) g).symm

Premises used: Equiv.symm_apply_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, Eq.symm, DFunLike.coe
-- 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
𝒢 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : 𝒢 ⟶ ℱ
g : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
⊢ Eq (α := G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : 𝒢 ⟶ ℱ'.obj) → G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj) (f ≫ g) :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    (G.op.whiskerLeft f ≫ (Equiv.symm restrictHomEquivHom : (a : ℱ ⟶ ℱ'.obj) → G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) g :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
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
𝒢 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : 𝒢 ⟶ ℱ
g : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
a :
  Eq (α := G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : 𝒢 ⟶ ℱ'.obj) → G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj) → 𝒢 ⟶ ℱ'.obj) (G.op.whiskerLeft f ≫ g)) :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : 𝒢 ⟶ ℱ'.obj) → G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj)
        (f ≫ (restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) g) :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
⊢ Eq (α := 𝒢 ⟶ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((restrictHomEquivHom : (a : G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj) → 𝒢 ⟶ ℱ'.obj) (G.op.whiskerLeft f ≫ g) :
      𝒢 ⟶ ℱ'.obj (P := Presheaf.IsSheaf K))
    (f ≫ (restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) g : 𝒢 ⟶ ℱ'.obj (P := Presheaf.IsSheaf K))

Tactic:
apply (restrictHomEquivHom (G := G)).symm.injective

Premises used: Equiv.injective, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, Equiv.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
𝒢 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : 𝒢 ⟶ ℱ
g : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
⊢ Eq (α := G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : 𝒢 ⟶ ℱ'.obj) → G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj)
        ((restrictHomEquivHom : (a : G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj) → 𝒢 ⟶ ℱ'.obj) (G.op.whiskerLeft f ≫ g)) :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))
    ((Equiv.symm restrictHomEquivHom : (a : 𝒢 ⟶ ℱ'.obj) → G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj)
        (f ≫ (restrictHomEquivHom : (a : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj) → ℱ ⟶ ℱ'.obj) g) :
      G.op ⋙ 𝒢 ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K))

Tactic:
simpa only [Equiv.symm_apply_apply] using
    (restrictHomEquivHom_naturality_left_symm (G := G) (f := f)
      (g := restrictHomEquivHom g)).symm

Premises used: Equiv.symm_apply_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, Eq.symm, DFunLike.coe, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ IsIso (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom

Tactic:
(sheafIso (asIso (whiskerLeft G.op α.hom))).isIso_hom

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.IsCoverDense.sheafIso, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Iso.isIso_hom, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.asIso