[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ U},
    (fun V i => ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s) Y f_1 →
      ∀ (g : Z ⟶ Y), (fun V i => ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s) Z (g ≫ f_1)
[PROOFSTEP]
rintro V W i ⟨t, ht⟩ j
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
V W : C
i : V ⟶ U
t : (forget A).obj (F.obj (op V))
ht : ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s
j : W ⟶ V
⊢ ∃ t, ↑(NatTrans.app f (op W)) t = ↑(G.map (j ≫ i).op) s
[PROOFSTEP]
refine' ⟨F.map j.op t, _⟩
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (G.obj (op U))
V W : C
i : V ⟶ U
t : (forget A).obj (F.obj (op V))
ht : ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) s
j : W ⟶ V
⊢ ↑(NatTrans.app f (op W)) (↑(F.map j.op) t) = ↑(G.map (j ≫ i).op) s
[PROOFSTEP]
rw [op_comp, G.map_comp, comp_apply, ← ht, elementwise_of% f.naturality]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
⊢ imageSieve f (↑(NatTrans.app f (op U)) s) = ⊤
[PROOFSTEP]
ext V i
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
⊢ (imageSieve f (↑(NatTrans.app f (op U)) s)).arrows i ↔ ⊤.arrows i
[PROOFSTEP]
simp only [Sieve.top_apply, iff_true_iff, imageSieve_apply]
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
⊢ ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) (↑(NatTrans.app f (op U)) s)
[PROOFSTEP]
have := elementwise_of% (f.naturality i.op)
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : (forget A).obj (F.obj (op U))
V : C
i : V ⟶ U
this :
  ∀ (x : (forget A).obj (F.obj (op U))),
    ↑(NatTrans.app f (op V)) (↑(F.map i.op) x) = ↑(G.map i.op) (↑(NatTrans.app f (op U)) x)
⊢ ∃ t, ↑(NatTrans.app f (op V)) t = ↑(G.map i.op) (↑(NatTrans.app f (op U)) s)
[PROOFSTEP]
exact ⟨F.map i.op s, this s⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤
[PROOFSTEP]
simp only [Subpresheaf.ext_iff, Function.funext_iff, Set.ext_iff, top_subpresheaf_obj, Set.top_eq_univ, Set.mem_univ,
  iff_true_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔
    ∀ (a : Cᵒᵖ) (x : (G ⋙ forget A).obj a),
      x ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A)))) a
[PROOFSTEP]
exact ⟨fun H U => H (unop U), fun H U => H (op U)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf f) = ⊤
[PROOFSTEP]
simp only [Subpresheaf.ext_iff, Function.funext_iff, Set.ext_iff, top_subpresheaf_obj, Set.top_eq_univ, Set.mem_univ,
  iff_true_iff]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ ∀ (a : Cᵒᵖ) (x : G.obj a), x ∈ Subpresheaf.obj (Subpresheaf.sheafify J (imagePresheaf f)) a
[PROOFSTEP]
exact ⟨fun H U => H (unop U), fun H U => H (op U)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallySurjective J f.val ↔ IsIso (imageSheafι f)
[PROOFSTEP]
rw [imageSheafι, isLocallySurjective_iff_imagePresheaf_sheafify_eq_top', Subpresheaf.eq_top_iff_isIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val))) ↔
    IsIso { val := Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf f.val)) }
[PROOFSTEP]
exact
  ⟨fun h => @isIso_of_reflects_iso _ _ _ _ _ _ (imageSheafι f) (sheafToPresheaf J _) h _, fun h =>
    @Functor.map_isIso _ _ _ _ _ _ (sheafToPresheaf J _) _ h⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))
[PROOFSTEP]
simp only [isLocallySurjective_iff_imagePresheaf_sheafify_eq_top]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤ ↔
    Subpresheaf.sheafify J (imagePresheaf (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
⊢ IsLocallySurjective J f
[PROOFSTEP]
intro U s
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
s : (forget A).obj (G.obj (op U))
⊢ imageSieve f s ∈ sieves J U
[PROOFSTEP]
obtain ⟨t, rfl⟩ := H _ s
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
t : (forget A).obj (F.obj (op U))
⊢ imageSieve f (↑(NatTrans.app f (op U)) t) ∈ sieves J U
[PROOFSTEP]
rw [imageSieve_app]
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
U : C
t : (forget A).obj (F.obj (op U))
⊢ ⊤ ∈ sieves J U
[PROOFSTEP]
exact J.top_mem _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
⊢ IsLocallySurjective J f
[PROOFSTEP]
apply isLocallySurjective_of_surjective
[GOAL]
case H
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
⊢ ∀ (U : Cᵒᵖ), Function.Surjective ↑(NatTrans.app f U)
[PROOFSTEP]
intro U
[GOAL]
case H
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Surjective ↑(NatTrans.app f U)
[PROOFSTEP]
apply Function.Bijective.surjective
[GOAL]
case H.hf
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Bijective ↑(NatTrans.app f U)
[PROOFSTEP]
rw [← isIso_iff_bijective, ← forget_map_eq_coe]
[GOAL]
case H.hf
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : ConcreteCategory A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ IsIso ((forget A).map (NatTrans.app f U))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂)
[PROOFSTEP]
intro U s
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
⊢ imageSieve (f₁ ≫ f₂) s ∈ sieves J U
[PROOFSTEP]
have : (Sieve.bind (imageSieve f₂ s) fun _ _ h => imageSieve f₁ h.choose) ≤ imageSieve (f₁ ≫ f₂) s :=
  by
  rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
  refine' ⟨t', _⟩
  rw [op_comp, F₃.map_comp, NatTrans.comp_app, comp_apply, comp_apply, ht', elementwise_of% f₂.naturality,
    H.choose_spec]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
⊢ (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
[PROOFSTEP]
rintro V i ⟨W, i, j, H, ⟨t', ht'⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve f₂ s).arrows j
t' : (forget A).obj (F₁.obj (op V))
ht' : ↑(NatTrans.app f₁ (op V)) t' = ↑(F₂.map i.op) (Exists.choose H)
⊢ (imageSieve (f₁ ≫ f₂) s).arrows (i ≫ j)
[PROOFSTEP]
refine' ⟨t', _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
V W : C
i : V ⟶ W
j : W ⟶ U
H : (imageSieve f₂ s).arrows j
t' : (forget A).obj (F₁.obj (op V))
ht' : ↑(NatTrans.app f₁ (op V)) t' = ↑(F₂.map i.op) (Exists.choose H)
⊢ ↑(NatTrans.app (f₁ ≫ f₂) (op V)) t' = ↑(F₃.map (i ≫ j).op) s
[PROOFSTEP]
rw [op_comp, F₃.map_comp, NatTrans.comp_app, comp_apply, comp_apply, ht', elementwise_of% f₂.naturality, H.choose_spec]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ imageSieve (f₁ ≫ f₂) s ∈ sieves J U
[PROOFSTEP]
apply J.superset_covering this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ∈ sieves J U
[PROOFSTEP]
apply J.bind_covering
[GOAL]
case hS
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ imageSieve f₂ s ∈ sieves J U
[PROOFSTEP]
apply h₂
[GOAL]
case hR
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U⦄ (H : (imageSieve f₂ s).arrows f), imageSieve f₁ (Exists.choose H) ∈ sieves J Y
[PROOFSTEP]
intros
[GOAL]
case hR
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
h₁ : IsLocallySurjective J f₁
h₂ : IsLocallySurjective J f₂
U : C
s : (forget A).obj (F₃.obj (op U))
this : (Sieve.bind (imageSieve f₂ s).arrows fun x x_1 h => imageSieve f₁ (Exists.choose h)) ≤ imageSieve (f₁ ≫ f₂) s
Y✝ : C
f✝ : Y✝ ⟶ U
H✝ : (imageSieve f₂ s).arrows f✝
⊢ imageSieve f₁ (Exists.choose H✝) ∈ sieves J Y✝
[PROOFSTEP]
apply h₁
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ toSheafify J F ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    toSheafify J F ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
simp [toImagePresheafSheafify]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
        (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) =
    𝟙 (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))
[PROOFSTEP]
rw [← cancel_mono (Subpresheaf.ι _), Category.id_comp, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F)))
[PROOFSTEP]
refine' Eq.trans _ (Category.comp_id _)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
        (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
      Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    𝟙 (sheafify J F)
[PROOFSTEP]
exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : ConcreteCategory A
F : Cᵒᵖ ⥤ Type (max u v)
⊢ toSheafify J F ≫
      sheafifyLift J (toImagePresheafSheafify J (toSheafify J F))
          (_ : Presheaf.IsSheaf J (Subpresheaf.toPresheaf (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))))) ≫
        Subpresheaf.ι (Subpresheaf.sheafify J (imagePresheaf (toSheafify J F))) =
    toSheafify J F ≫ 𝟙 (sheafify J F)
[PROOFSTEP]
simp [toImagePresheafSheafify]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J F)
[PROOFSTEP]
rw [isLocallySurjective_iff_whisker_forget, ← toSheafify_comp_sheafifyCompIso_inv]
[GOAL]
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J (F ⋙ forget B) ≫ (sheafifyCompIso J (forget B) F).inv)
[PROOFSTEP]
apply IsLocallySurjective.comp
[GOAL]
case h₁
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (toSheafify J (F ⋙ forget B))
[PROOFSTEP]
rw [isLocallySurjective_iff_imagePresheaf_sheafify_eq_top, Subpresheaf.eq_top_iff_isIso]
[GOAL]
case h₁
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsIso
    (Subpresheaf.ι
      (Subpresheaf.sheafify J (imagePresheaf (whiskerRight (toSheafify J (F ⋙ forget B)) (forget (Type (max u v)))))))
[PROOFSTEP]
exact IsIso.of_iso_inv (sheafificationIsoImagePresheaf J (F ⋙ forget B))
[GOAL]
case h₂
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : ConcreteCategory A
F✝ : Cᵒᵖ ⥤ Type (max u v)
B : Type w
inst✝⁶ : Category.{max u v, w} B
inst✝⁵ : ConcreteCategory B
inst✝⁴ : ∀ (X : C), Limits.HasColimitsOfShape (Cover J X)ᵒᵖ B
inst✝³ : ∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : Cover J X), Limits.HasMultiequalizer (Cover.index S P)
inst✝² :
  (X : C) →
    (W : Cover J X) →
      (P : Cᵒᵖ ⥤ B) → Limits.PreservesLimit (Limits.MulticospanIndex.multicospan (Cover.index W P)) (forget B)
inst✝¹ : (X : C) → Limits.PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget B)
inst✝ : ∀ (α β : Type (max u v)) (fst snd : β → α), Limits.HasLimitsOfShape (Limits.WalkingMulticospan fst snd) B
F : Cᵒᵖ ⥤ B
⊢ IsLocallySurjective J (sheafifyCompIso J (forget B) F).inv
[PROOFSTEP]
exact isLocallySurjective_of_iso _ _
