Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
      {
        hom :=
          ⋯.extend
            {
              app := fun Y ↦
                ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
              naturality := ⋯ } } =
    s.inj j

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m =
    {
      hom :=
        ⋯.extend
          {
            app := fun Y ↦
              ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
            naturality := ⋯ } }

Tactic:
· ext : 1
    let u (j : ι) : CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows _ c.inj).functor :=
      (Sieve.ofArrows _ c.inj).toFunctor (c.inj j) (Sieve.ofArrows_mk _ _ j)
    have (j : ι) : u j ≫ (Sieve.ofArrows _ c.inj).functorInclusion =
      CategoryTheory.yoneda.map (c.inj j) := rfl
    dsimp
    simp only [← this, Category.assoc, Presieve.IsSheafFor.functorInclusion_comp_extend]
    ext Z (g : Z.unop ⟶ X j)
    have h : Sieve.ofArrows X c.inj (g ≫ c.inj j) :=
      Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ j) _
    exact heq s (Sieve.ofArrows.h h) g (by simp)

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m =
    {
      hom :=
        ⋯.extend
          {
            app := fun Y ↦
              ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
            naturality := ⋯ } }