[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
⊢ Function.LeftInverse
    (fun γ =>
      {
        val :=
          sheafifyLift J
            (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
            (_ : Presheaf.IsSheaf J Y.val) })
    fun η =>
    {
      val :=
        ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
          (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) }
[PROOFSTEP]
intro η
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ (fun γ =>
        {
          val :=
            sheafifyLift J
              (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
              (_ : Presheaf.IsSheaf J Y.val) })
      ((fun η =>
          {
            val :=
              ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
        η) =
    η
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ ((fun γ =>
          {
            val :=
              sheafifyLift J
                (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                (_ : Presheaf.IsSheaf J Y.val) })
        ((fun η =>
            {
              val :=
                ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                  (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
          η)).val =
    η.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ sheafifyLift J
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val)))
      (_ : Presheaf.IsSheaf J Y.val) =
    η.val
[PROOFSTEP]
symm
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ η.val =
    sheafifyLift J
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val)))
      (_ : Presheaf.IsSheaf J Y.val)
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case h.a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
η : (composeAndSheafify J G).obj X ⟶ Y
⊢ toSheafify J (X.val ⋙ G) ≫ η.val =
    ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val))
[PROOFSTEP]
rw [Equiv.symm_apply_apply]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
⊢ Function.RightInverse
    (fun γ =>
      {
        val :=
          sheafifyLift J
            (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
            (_ : Presheaf.IsSheaf J Y.val) })
    fun η =>
    {
      val :=
        ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
          (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) }
[PROOFSTEP]
intro γ
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ (fun η =>
        {
          val :=
            ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
              (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
      ((fun γ =>
          {
            val :=
              sheafifyLift J
                (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                (_ : Presheaf.IsSheaf J Y.val) })
        γ) =
    γ
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ ((fun η =>
          {
            val :=
              ↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val)
                (toSheafify J (((whiskeringRight Cᵒᵖ E D).obj G).obj ((sheafToPresheaf J E).obj X)) ≫ η.val) })
        ((fun γ =>
            {
              val :=
                sheafifyLift J
                  (↑(Adjunction.homEquiv A ((sheafToPresheaf J E).obj X) Y.val).symm ((sheafToPresheaf J E).map γ))
                  (_ : Presheaf.IsSheaf J Y.val) })
          γ)).val =
    γ.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X : Sheaf J E
Y : Sheaf J D
A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj
γ : X ⟶ (sheafCompose J F).obj Y
⊢ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val)
      (toSheafify J (X.val ⋙ G) ≫
        sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X.val Y.val).symm γ.val)
          (_ : Presheaf.IsSheaf J Y.val)) =
    γ.val
[PROOFSTEP]
rw [J.toSheafify_sheafifyLift, Equiv.apply_symm_apply]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ ↑(composeEquiv J adj X'✝ Y✝).symm (f ≫ g) = (composeAndSheafify J G).map f ≫ ↑(composeEquiv J adj X✝ Y✝).symm g
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ (↑(composeEquiv J adj X'✝ Y✝).symm (f ≫ g)).val =
    ((composeAndSheafify J G).map f ≫ ↑(composeEquiv J adj X✝ Y✝).symm g).val
[PROOFSTEP]
dsimp [composeEquiv]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X'✝.val Y✝.val).symm (f.val ≫ g.val))
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyMap J (whiskerRight f.val G) ≫
      sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
        (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rw [sheafifyMap_sheafifyLift]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X'✝.val Y✝.val).symm (f.val ≫ g.val))
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
erw [Adjunction.homEquiv_naturality_left_symm]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J
      (((whiskeringRight Cᵒᵖ E D).obj G).map f.val ≫
        ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rw [whiskeringRight_obj_map]
[GOAL]
case h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X'✝ X✝ : Sheaf J E
Y✝ : Sheaf J D
f : X'✝ ⟶ X✝
g : X✝ ⟶ (sheafCompose J F).obj Y✝
⊢ sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val) =
    sheafifyLift J
      (whiskerRight f.val G ≫ ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val).symm g.val)
      (_ : Presheaf.IsSheaf J Y✝.val)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
⊢ ↑(composeEquiv J adj X✝ Y'✝) (f ≫ g) = ↑(composeEquiv J adj X✝ Y✝) f ≫ (sheafCompose J F).map g
[PROOFSTEP]
ext
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app (↑(composeEquiv J adj X✝ Y'✝) (f ≫ g)).val x✝ =
    NatTrans.app (↑(composeEquiv J adj X✝ Y✝) f ≫ (sheafCompose J F).map g).val x✝
[PROOFSTEP]
dsimp [composeEquiv]
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app
      (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y'✝.val)
        (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val))
      x✝ =
    NatTrans.app
        (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) X✝.val Y✝.val) (toSheafify J (X✝.val ⋙ G) ≫ f.val))
        x✝ ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
erw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app
      (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val ≫
        ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val))
      x✝ =
    NatTrans.app
        (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val ≫
          ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val))
        x✝ ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w.h
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
adj : G ⊣ F
X✝ : Sheaf J E
Y✝ Y'✝ : Sheaf J D
f : (composeAndSheafify J G).obj X✝ ⟶ Y✝
g : Y✝ ⟶ Y'✝
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val) x✝ ≫
      F.map (NatTrans.app (toSheafify J (X✝.val ⋙ G)) x✝ ≫ NatTrans.app f.val x✝ ≫ NatTrans.app g.val x✝) =
    (NatTrans.app (NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit X✝.val) x✝ ≫
        F.map (NatTrans.app (toSheafify J (X✝.val ⋙ G)) x✝ ≫ NatTrans.app f.val x✝)) ≫
      F.map (NatTrans.app g.val x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (adjunctionToTypes J adj).unit Y).val =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit ((sheafOfTypesToPresheaf J).obj Y) ≫
      whiskerRight
        (toSheafify J (((whiskeringRight Cᵒᵖ (Type (max v u)) D).obj G).obj ((sheafOfTypesToPresheaf J).obj Y)))
        (forget D)
[PROOFSTEP]
dsimp [adjunctionToTypes, Adjunction.comp]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit Y).val ≫
      (NatTrans.app (adjunction J adj).unit ((sheafEquivSheafOfTypes J).inverse.obj Y)).val ≫
        𝟙 (sheafify J (Y.val ⋙ G) ⋙ forget D) =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit Y).val ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Y.val (sheafify J (Y.val ⋙ G)))
        (toSheafify J (Y.val ⋙ G)) =
    NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).unit Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ (NatTrans.app (adjunctionToTypes J adj).counit X).val =
    sheafifyLift J
      ((Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1)
      (_ : Presheaf.IsSheaf J X.val)
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app (adjunctionToTypes J adj).counit X).val =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
dsimp only [adjunctionToTypes, Adjunction.comp, NatTrans.comp_app, instCategorySheaf_comp_val, instCategorySheaf_id_val]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app
            (Functor.associator (sheafCompose J (forget D)) (Equivalence.symm (sheafEquivSheafOfTypes J)).inverse
                ((Equivalence.symm (sheafEquivSheafOfTypes J)).functor ⋙ composeAndSheafify J G)).hom
            X).val ≫
        (NatTrans.app
              (whiskerLeft (sheafCompose J (forget D))
                (whiskerRight (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  (composeAndSheafify J G)))
              X).val ≫
          (NatTrans.app (adjunction J adj).counit X).val =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
rw [adjunction_counit_app_val]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ toSheafify J
        (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫
      (NatTrans.app
            (Functor.associator (sheafCompose J (forget D)) (Equivalence.symm (sheafEquivSheafOfTypes J)).inverse
                ((Equivalence.symm (sheafEquivSheafOfTypes J)).functor ⋙ composeAndSheafify J G)).hom
            X).val ≫
        (NatTrans.app
              (whiskerLeft (sheafCompose J (forget D))
                (whiskerRight (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  (composeAndSheafify J G)))
              X).val ≫
          sheafifyLift J
            (↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm
              (𝟙 (X.val ⋙ forget D)))
            (_ : Presheaf.IsSheaf J X.val) =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
erw [Category.id_comp, J.sheafifyMap_sheafifyLift, J.toSheafify_sheafifyLift]
[GOAL]
case a
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
⊢ ((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).map
        ((sheafToPresheaf J (Type (max u v))).map
          (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
            ((sheafCompose J (forget D)).obj X))) ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm (𝟙 (X.val ⋙ forget D)) =
    (Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1
[PROOFSTEP]
ext
[GOAL]
case a.w.h.w
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
x✝¹ : Cᵒᵖ
x✝ :
  (forget D).obj
    ((((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj
            (((Equivalence.symm (sheafEquivSheafOfTypes J)).inverse ⋙
                  (Equivalence.symm (sheafEquivSheafOfTypes J)).functor).obj
              ((sheafCompose J (forget D)).obj X)))).obj
      x✝¹)
⊢ ↑(NatTrans.app
          (((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).map
              ((sheafToPresheaf J (Type (max u v))).map
                (NatTrans.app (Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).counit
                  ((sheafCompose J (forget D)).obj X))) ≫
            ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) (X.val ⋙ forget D) X.val).symm
              (𝟙 (X.val ⋙ forget D)))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          ((Functor.associator X.1 (forget D) G).hom ≫ NatTrans.app (Adjunction.whiskerRight Cᵒᵖ adj).counit X.1) x✝¹)
      x✝
[PROOFSTEP]
dsimp [sheafEquivSheafOfTypes, Equivalence.symm, Equivalence.toAdjunction, NatIso.ofComponents, Adjunction.whiskerRight,
  Adjunction.mkOfUnitCounit]
[GOAL]
case a.w.h.w
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁷ : Category.{max v u, w₂} E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
X : Sheaf J D
x✝¹ : Cᵒᵖ
x✝ :
  (forget D).obj
    ((((whiskeringRight Cᵒᵖ (Type (max u v)) D).obj G).obj
          ((sheafToPresheaf J (Type (max u v))).obj
            (((Equivalence.symm (sheafEquivSheafOfTypes J)).inverse ⋙
                  (Equivalence.symm (sheafEquivSheafOfTypes J)).functor).obj
              ((sheafCompose J (forget D)).obj X)))).obj
      x✝¹)
⊢ ↑(G.map (𝟙 ((forget D).obj (X.val.obj x✝¹))) ≫
          G.map (𝟙 ((forget D).obj (X.val.obj x✝¹))) ≫
            𝟙 (G.obj ((forget D).obj (X.val.obj x✝¹))) ≫ NatTrans.app adj.counit (X.val.obj x✝¹) ≫ 𝟙 (X.val.obj x✝¹))
      x✝ =
    ↑(𝟙 (G.obj ((forget D).obj (X.1.obj x✝¹))) ≫
          𝟙 (G.obj ((forget D).obj (X.1.obj x✝¹))) ≫ NatTrans.app adj.counit (X.1.obj x✝¹) ≫ 𝟙 (X.val.obj x✝¹))
      x✝
[PROOFSTEP]
simp
