-- Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
lemma Sheaf.isConstant_of_forget [constantSheaf J D |>.Faithful] [constantSheaf J D |>.Full]
    [constantSheaf J B |>.Faithful] [constantSheaf J B |>.Full]
    [(sheafCompose J U).ReflectsIsomorphisms] [((sheafCompose J U).obj F).IsConstant J]
    {T : C} (hT : IsTerminal T) : F.IsConstant J

Proof state:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsConstant J F

Tactic:
have : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) := by
  rw [← constantSheafAdj_counit_w]
  infer_instance

Result:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsConstant J F

Proof state:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)

Tactic:
exact isIso_of_reflects_iso _ (sheafCompose J U)

Result:
no goals

Proof state:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))

Tactic:
rw [← constantSheafAdj_counit_w]

Result:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
⊢ IsIso
    ((constantCommuteCompose J U).hom.app (F.val.obj (op T)) ≫
      (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F))

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

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsConstant J F

Tactic:
rw [F.isConstant_iff_isIso_counit_app (hT := hT)]

Result:
C : Type u_1
inst✝¹² : Category.{u_5, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝¹¹ : Category.{u_4, u_2} D
inst✝¹⁰ : HasWeakSheafify J D
B : Type u_3
inst✝⁹ : Category.{u_6, u_3} B
U : D ⥤ B
inst✝⁸ : HasWeakSheafify J B
inst✝⁷ : J.PreservesSheafification U
inst✝⁶ : J.HasSheafCompose U
F : Sheaf J D
inst✝⁵ : (constantSheaf J D).Faithful
inst✝⁴ : (constantSheaf J D).Full
inst✝³ : (constantSheaf J B).Faithful
inst✝² : (constantSheaf J B).Full
inst✝¹ : (sheafCompose J U).ReflectsIsomorphisms
inst✝ : IsConstant J ((sheafCompose J U).obj F)
T : C
hT : IsTerminal T
this : IsIso ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)