C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
⊢ (∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))) ↔
    ∀ (X : C) (S : GrothendieckTopology.Cover J X), IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
⊢ IsSheaf J P ↔ ∀ (X : C) (S : GrothendieckTopology.Cover J X), IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
rw [isSheaf_iff_multifork]
case refine'_1
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P)) →
    IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)

case refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P) →
    Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
⊢ (∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))) ↔
    ∀ (X : C) (S : GrothendieckTopology.Cover J X), IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
refine' forall₂_congr fun X S => ⟨_, _⟩
case refine'_1.intro
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
case refine'_1
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P)) →
    IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
rintro ⟨h⟩
case refine'_1.intro
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
e : P.obj X.op ≅ multiequalizer (GrothendieckTopology.Cover.index S P) :=
  IsLimit.conePointUniqueUpToIso h (limit.isLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)))
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
case refine'_1.intro
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
let e : P.obj (op X) ≅ multiequalizer (S.index P) :=
  h.conePointUniqueUpToIso (limit.isLimit _)
no goals
case refine'_1.intro
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
e : P.obj X.op ≅ multiequalizer (GrothendieckTopology.Cover.index S P) :=
  IsLimit.conePointUniqueUpToIso h (limit.isLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)))
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
exact (inferInstance : IsIso e.hom)
case refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
case refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
⊢ IsIso (GrothendieckTopology.Cover.toMultiequalizer S P) →
    Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
intro h
case refine'_2.refine'_1
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).pt ≅
    (GrothendieckTopology.Cover.multifork S P).pt

case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ ∀ (j : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo),
    (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app j =
      ?refine'_2.refine'_1.hom ≫ (GrothendieckTopology.Cover.multifork S P).π.app j
case refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
refine' ⟨IsLimit.ofIsoLimit (limit.isLimit _) (Cones.ext _ _)⟩
no goals
case refine'_2.refine'_1
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).pt ≅
    (GrothendieckTopology.Cover.multifork S P).pt
apply (@asIso _ _ _ _ _ h).symm
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a =
    (asIso (GrothendieckTopology.Cover.toMultiequalizer S P)).symm.hom ≫
      (GrothendieckTopology.Cover.multifork S P).π.app a
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
⊢ ∀ (j : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo),
    (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app j =
      (asIso (GrothendieckTopology.Cover.toMultiequalizer S P)).symm.hom ≫
        (GrothendieckTopology.Cover.multifork S P).π.app j
intro a
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (asIso (GrothendieckTopology.Cover.toMultiequalizer S P)).symm.hom ≫
      (GrothendieckTopology.Cover.multifork S P).π.app a =
    (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a =
    (asIso (GrothendieckTopology.Cover.toMultiequalizer S P)).symm.hom ≫
      (GrothendieckTopology.Cover.multifork S P).π.app a
symm
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (GrothendieckTopology.Cover.multifork S P).π.app a =
    GrothendieckTopology.Cover.toMultiequalizer S P ≫
      (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (asIso (GrothendieckTopology.Cover.toMultiequalizer S P)).symm.hom ≫
      (GrothendieckTopology.Cover.multifork S P).π.app a =
    (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a
erw [IsIso.inv_comp_eq]
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (match a with
    | WalkingMulticospan.left a => P.map a.f.op
    | WalkingMulticospan.right b =>
      P.map (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index S P) b).f.op ≫
        MulticospanIndex.fst (GrothendieckTopology.Cover.index S P) b) =
    GrothendieckTopology.Cover.toMultiequalizer S P ≫
      limit.π (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) a
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (GrothendieckTopology.Cover.multifork S P).π.app a =
    GrothendieckTopology.Cover.toMultiequalizer S P ≫
      (limit.cone (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P))).π.app a
dsimp
no goals
case refine'_2.refine'_2
C : Type u₁
inst✝² : Category C
A : Type u₂
inst✝¹ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : GrothendieckTopology.Cover J X), HasMultiequalizer (GrothendieckTopology.Cover.index S P)
X : C
S : GrothendieckTopology.Cover J X
h : IsIso (GrothendieckTopology.Cover.toMultiequalizer S P)
a : WalkingMulticospan (GrothendieckTopology.Cover.index S P).fstTo (GrothendieckTopology.Cover.index S P).sndTo
⊢ (match a with
    | WalkingMulticospan.left a => P.map a.f.op
    | WalkingMulticospan.right b =>
      P.map (MulticospanIndex.fstTo (GrothendieckTopology.Cover.index S P) b).f.op ≫
        MulticospanIndex.fst (GrothendieckTopology.Cover.index S P) b) =
    GrothendieckTopology.Cover.toMultiequalizer S P ≫
      limit.π (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) a
simp