-- Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
/-- The counit of `constantSheafAdj` factors through the isomorphism `constantCommuteCompose`. -/
lemma constantSheafAdj_counit_w {T : C} (hT : IsTerminal T) :
    ((constantCommuteCompose J U).hom.app (F.val.obj ⟨T⟩)) ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) =
        ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))

Proof state:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ U.map (F.val.map (hT.from (unop x✝)).op) =
    U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)))).app x✝) ≫
      U.map (((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val)).val.app x✝) ≫
        U.map ((sheafifyLift J (𝟙 F.val) ⋯).app x✝)

Tactic:
simp [← map_comp, ← NatTrans.comp_app]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ (constantCommuteCompose J U).hom.app (F.val.obj (op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F) =
    (sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)

Tactic:
apply Sheaf.hom_ext

Result:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ ((constantCommuteCompose J U).hom.app (F.val.obj (op T)) ≫
        (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val

Proof state:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
      sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
        ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
      (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
        ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val

Tactic:
ext

Result:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
            ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val).app
      x✝ =
    (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
            ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val).app
      x✝

Proof state:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
            ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val).app
      x✝ =
    (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
            ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val).app
      x✝

Tactic:
simp only [comp_obj, const_obj_obj, sheafCompose_obj_val, id_obj,
constantSheafAdj_counit_app, instCategorySheaf_comp_val,
sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift, comp_id,
toSheafify_sheafifyLift, NatTrans.comp_app, constComp_hom_app,
constantPresheafAdj_counit_app_app, Functor.comp_map, id_comp, flip_obj_obj,
sheafToPresheaf_obj, map_comp, sheafCompose_map_val, sheafComposeIso_hom_fac_assoc,
whiskerRight_app]

Result:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ U.map (F.val.map (hT.from (unop x✝)).op) =
    U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)))).app x✝) ≫
      U.map (((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val)).val.app x✝) ≫
        U.map ((sheafifyLift J (𝟙 F.val) ⋯).app x✝)

Proof state:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
            ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val).app
      x✝ =
    (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
          (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
            ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val).app
      x✝

Tactic:
simp? says simp only [comp_obj, const_obj_obj, sheafCompose_obj_val, id_obj,
    constantSheafAdj_counit_app, instCategorySheaf_comp_val,
    sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift, comp_id,
    toSheafify_sheafifyLift, NatTrans.comp_app, constComp_hom_app,
    constantPresheafAdj_counit_app_app, Functor.comp_map, id_comp, flip_obj_obj,
    sheafToPresheaf_obj, map_comp, sheafCompose_map_val, sheafComposeIso_hom_fac_assoc,
    whiskerRight_app]

Result:
case h.w.h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
x✝ : Cᵒᵖ
⊢ U.map (F.val.map (hT.from (unop x✝)).op) =
    U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)))).app x✝) ≫
      U.map (((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val)).val.app x✝) ≫
        U.map ((sheafifyLift J (𝟙 F.val) ⋯).app x✝)