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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ 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))
have 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
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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
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
have 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)
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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.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)
have 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)
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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.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)
have 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)
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
α : ℱ ⟶ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
⊢ 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)
have w : (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x).Compatible (R :=
  Sieve.arrows (Sieve.coverByImage G (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
α : ℱ ⟶ ℱ'.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)))
⊢ 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)
have 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)
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
α : ℱ ⟶ ℱ'.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
| ((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)))
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 (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]
-- 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ᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (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
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 (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]
-- 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ᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda (ℱ.obj X)) U
Y : D
f : Y ⟶ unop X
hf : Sieve.arrows (Sieve.coverByImage G (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 (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
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 (G.obj (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
f : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
𝒢' : Sheaf.{v_2, v_4, u_2, u_4} K A
g : ℱ' ⟶ 𝒢'
⊢ 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))
have 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))
Tactic: apply (restrictHomEquivHom (G := G)).symm.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
𝒢 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : 𝒢 ⟶ ℱ
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))
have 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))
Tactic: apply (restrictHomEquivHom (G := G)).symm.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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ IsIso α
have h : α = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom
Tactic: convert! (sheafIso (asIso (whiskerLeft G.op α.hom))).isIso_hom using 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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ α = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom
have h : α.hom = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom.hom
Tactic: ext1
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
⊢ CompatiblePreserving K G
have compatible : ∀ (ℱ : Sheaf K (Type u_5)) {Z : C} {T : Presieve.{v_1, u_1} Z}
  {x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T},
  x.Compatible (R := T) →
    ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂),
      f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
        Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                  (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
              (x g₁ hg₁) :
            (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                  (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
              (x g₂ hg₂) :
            (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
Tactic: constructor
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
        (x g₁ hg₁) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
        (x g₂ hg₂) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
have compatible : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
  Eq (α := (fun (X : Type u_5) ↦ 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 u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
            (x g₁ hg₁) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      (fun (X : Type u_5) ↦ 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 u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
            (x g₂ hg₂) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
Tactic: apply Functor.IsCoverDense.ext G