awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
inst_8 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
⊢ Eq.{w' + 1} (α :=
    (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) F).obj (P := Presheaf.IsSheaf J).obj x ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x)
    (NatTrans.app (InducedCategory.Hom.hom 0) x)
have h : ∀ (j : (J.Cover (unop x))ᵒᵖ),
  Eq (α :=
    Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j)
      (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j) (NatTrans.app (InducedCategory.Hom.hom 0) x))
Tactic: refine colimit.hom_ext (fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
inst_8 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
j : (J.Cover (unop x))ᵒᵖ
⊢ Eq (α :=
    Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j)
      (NatTrans.app (InducedCategory.Hom.hom (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) 0)) x))
    (CategoryStruct.comp (Y := colimit (J := (J.Cover (unop x))ᵒᵖ) (J.diagram (J.plusObj F) (unop x)))
      (colimit.ι (J.diagram (J.plusObj F) (unop x)) j) (NatTrans.app (InducedCategory.Hom.hom 0) x))
have h : Eq (α :=
  Functor.obj (J.diagram (J.plusObj F) (unop x)) j ⟶
    (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) G).obj (P := Presheaf.IsSheaf J).obj x)
  (NatTrans.app (J.diagramNatTrans (J.plusMap 0) (unop x)) j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x)) j) 0
Tactic: erw [colimit.ι_map, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
⊢ Eq (α :=
    (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
      R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        ((Equiv.symm
              { toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P ⟶ R) ↦ J.toSheafify P ≫ e.hom,
                invFun := fun (e : P ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
            (a : P ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj P ⟶ R)
          (η ≫ γ)) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
        (Functor.map (plusPlusSheaf J D (FD := FD) (CD := CD)) η ≫
          (Equiv.symm
                {
                  toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) Q ⟶ R) ↦
                    J.toSheafify Q ≫ e.hom,
                  invFun := fun (e : Q ⟶ Functor.obj (sheafToPresheaf J D) R) ↦ { hom := J.sheafifyLift e ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
              (a : Q ⟶ (sheafToPresheaf J D).obj R) → (plusPlusSheaf J D).obj Q ⟶ R)
            γ) :
      (Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) P).obj (P := Presheaf.IsSheaf J) ⟶
        R.obj (P := Presheaf.IsSheaf J))
have h : Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyLift (η ≫ γ) sorry)
  (J.sheafifyMap η ≫ J.sheafifyLift γ sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P Q : Functor.{v, w', u, w} Cᵒᵖ D
R : Sheaf.{v, w', u, w} J D
η : P ⟶ Q
γ : Q ⟶ Functor.obj (sheafToPresheaf J D) R
⊢ Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyLift (η ≫ γ) ⋯)
    (J.sheafifyMap η ≫ J.sheafifyLift γ ⋯)
have h : Eq (α := J.sheafify P ⟶ R.obj (P := Presheaf.IsSheaf J)) (J.sheafifyMap η ≫ J.sheafifyLift γ sorry)
  (J.sheafifyLift (η ≫ γ) sorry)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
X : Functor.{v, w', u, w} Cᵒᵖ D
Y Y' : Sheaf.{v, w', u, w} J D
η : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y
γ : Y ⟶ Y'
⊢ Eq (α := X ⟶ Functor.obj (sheafToPresheaf J D) Y')
    (({ toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y') ↦ J.toSheafify X ≫ e.hom,
            invFun := fun (e : X ⟶ Functor.obj (sheafToPresheaf J D) Y') ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : (plusPlusSheaf J D).obj X ⟶ Y') → X ⟶ (sheafToPresheaf J D).obj Y')
        (η ≫ γ) :
      X ⟶ Functor.obj (sheafToPresheaf J D) Y')
    (({ toFun := fun (e : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y) ↦ J.toSheafify X ≫ e.hom,
              invFun := fun (e : X ⟶ Functor.obj (sheafToPresheaf J D) Y) ↦ { hom := J.sheafifyLift e ⋯ },
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (plusPlusSheaf J D).obj X ⟶ Y) → X ⟶ (sheafToPresheaf J D).obj Y)
          η ≫
        Functor.map (sheafToPresheaf J D) γ :
      X ⟶ Functor.obj (sheafToPresheaf J D) Y')
have dsimp : J.toSheafify X ≫ η.hom ≫ γ.hom = (J.toSheafify X ≫ η.hom) ≫ γ.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_5 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
X : Functor.{v, w', u, w} Cᵒᵖ D
Y Y' : Sheaf.{v, w', u, w} J D
η : Functor.obj (plusPlusSheaf J D (FD := FD) (CD := CD)) X ⟶ Y
γ : Y ⟶ Y'
⊢ J.toSheafify X ≫ η.hom ≫ γ.hom = (J.toSheafify X ≫ η.hom) ≫ γ.hom
have rw : J.toSheafify X ≫ η.hom ≫ γ.hom = J.toSheafify X ≫ η.hom ≫ γ.hom
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ Eq (α :=
    obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x_1)
    (map (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x_2 ≫
      match (motive :=
        (x : Cᵒᵖ) →
          obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
            (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x)
        x_1 with
      | Opposite.op X => F.map (hT.from X).op)
    ((match (motive :=
        (x : Cᵒᵖ) →
          obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) F) x ⟶
            (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).obj x)
        x with
      | Opposite.op X => F.map (hT.from X).op) ≫
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) F).map x_2)
have simp : F.map (Quiver.Hom.op (hT.from (Opposite.unop x_1))) = F.map (Quiver.Hom.op (hT.from (Opposite.unop x)) ≫ x_2)
Tactic: simp only [Functor.comp_obj, Functor.const_obj_obj, Functor.id_obj, Functor.const_obj_map,
          Category.id_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ F.map (Quiver.Hom.op (hT.from (Opposite.unop x_1))) = F.map (Quiver.Hom.op (hT.from (Opposite.unop x)) ≫ x_2)
have e_a : hT.from (Opposite.unop x_1) = x_2.unop ≫ Quiver.Hom.unop (Quiver.Hom.op (hT.from (Opposite.unop x)))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
T : C
hT : IsTerminal.{v_1, u_1} T
X Y : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : X ⟶ Y
⊢ Eq (α := obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X ⟶ obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y)
    (map (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) f ≫
      {
        app := fun (x : Cᵒᵖ) ↦
          match (motive :=
            (x : Cᵒᵖ) →
              obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) Y) x ⟶
                (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
            x with
          | Opposite.op X => Y.map (hT.from X).op,
        naturality := ⋯ })
    ({
        app := fun (x : Cᵒᵖ) ↦
          match (motive :=
            (x : Cᵒᵖ) →
              obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
                (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) X).obj x)
            x with
          | Opposite.op X_1 => X.map (hT.from X_1).op,
        naturality := ⋯ } ≫
      map (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) f)
have w : ∀ (x : Cᵒᵖ),
  Eq (α :=
    obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
    (NatTrans.app
      (map (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) f ≫
        {
          app := fun (x : Cᵒᵖ) ↦
            match (motive :=
              (x : Cᵒᵖ) →
                obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) Y) x ⟶
                  (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) Y).obj x)
              x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := sorry })
      x)
    (NatTrans.app
      ({
          app := fun (x : Cᵒᵖ) ↦
            match (motive :=
              (x : Cᵒᵖ) →
                obj.{v_1, v_2, u_1, u_2} (obj (obj (evaluation Cᵒᵖ D) (Opposite.op T) ⋙ const Cᵒᵖ) X) x ⟶
                  (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) X).obj x)
              x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := sorry } ≫
        map (𝟭 (Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D)) f)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
L : D ⥤ Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
adj : L ⊣ obj (sheafSections J D) (Opposite.op T)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
⊢ IsConstant J F ↔ L.essImage F
have rw : IsConstant J F ↔ essImage (constantSheaf J D) F
Tactic: rw [essImage_eq_of_natIso (adj.leftAdjointUniq (constantSheafAdj J D hT))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
inst_3 : Faithful (constantSheaf J D)
inst_4 : Full (constantSheaf J D)
F : Sheaf.{v_1, v_2, u_1, u_2} J D
inst_5 : IsConstant J F
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ IsIso (X := obj (obj (sheafSections J D) (Opposite.op T) ⋙ constantSheaf J D) F)
    (NatTrans.app (counit (constantSheafAdj J D hT)) F)
have rw : essImage (constantSheaf J D) F
Tactic: rw [isIso_counit_app_iff_mem_essImage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
⊢ IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) ↔ IsConstant K F
have mp : IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) → IsConstant K F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
C' : Type u_3
inst_3 : Category.{v_3, u_3} C'
K : GrothendieckTopology.{v_3, u_3} C'
inst_4 : HasWeakSheafify.{v_3, v_2, u_3, u_2} K D
G : Functor.{v_1, v_3, u_1, u_3} C C'
inst_5 : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst_6 : IsDenseSubsite J K G
T : C
hT : IsTerminal.{v_1, u_1} T
hT' : IsTerminal.{v_3, u_3} (G.obj T)
F : Sheaf.{v_3, v_2, u_3, u_2} K D
mp : IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) → IsConstant K F
⊢ IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F) ↔ IsConstant K F
have mpr : IsConstant K F → IsConstant J (obj (Equivalence.inverse (sheafEquiv J K G D)) F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ Eq (α :=
    (constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)) ⟶
      obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F))
    (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F)))
    ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F))
have h : Eq (α :=
  ((constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))).obj (P :=
      Presheaf.IsSheaf J) ⟶
    (obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F)).obj (P := Presheaf.IsSheaf J))
  (InducedCategory.Hom.hom
    (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
      (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))))
  (InducedCategory.Hom.hom ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F)))
Tactic: apply Sheaf.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConstantSheaf (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : HasWeakSheafify.{v_1, v_2, u_1, u_2} J D
B : Type u_3
inst_3 : Category.{v_3, u_3} B
U : Functor.{v_2, v_3, u_2, u_3} D B
inst_4 : HasWeakSheafify.{v_1, v_3, u_1, u_3} J B
inst_5 : J.PreservesSheafification U
inst_6 : J.HasSheafCompose U
F : Sheaf.{v_1, v_2, u_1, u_2} J D
T : C
hT : IsTerminal.{v_1, u_1} T
⊢ Eq (α :=
    ((constantSheaf J D ⋙ sheafCompose J U).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))).obj (P :=
        Presheaf.IsSheaf J) ⟶
      (obj (𝟭 (Sheaf.{v_1, v_3, u_1, u_3} J B)) ((sheafCompose J U).obj F)).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := (U ⋙ constantSheaf J B).obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))
        (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))))
    (InducedCategory.Hom.hom ((sheafCompose J U).map (NatTrans.app (counit (constantSheafAdj J D hT)) F)))
have h : Eq (α :=
  ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
        (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
      U ⟶
    F.obj (P := Presheaf.IsSheaf J) ⋙ U)
  (CategoryStruct.comp (Y :=
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
        (obj (constantSheaf J B) (U.obj (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T)))))
      (InducedCategory.Hom.hom
        (NatTrans.app (Iso.hom (constantCommuteCompose J U)) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))))
      (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J B hT)) ((sheafCompose J U).obj F))) :
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
  (whiskerRight (InducedCategory.Hom.hom (NatTrans.app (counit (constantSheafAdj J D hT)) F)) U :
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)
          (obj (constantSheaf J D) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op T))) ⋙
        U ⟶
      F.obj (P := Presheaf.IsSheaf J) ⋙ U)
Tactic: dsimp