C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
⊢ IsSheaf J (P ⋙ F)
rw [Presheaf.isSheaf_iff_multifork] at hP⊢
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
intro X S
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
obtain ⟨h⟩ := hP X S
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (F.mapCone (GrothendieckTopology.Cover.multifork S P))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
replace h := isLimitOfPreserves F h
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h :
  IsLimit
    ((Cones.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj
      (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (F.mapCone (GrothendieckTopology.Cover.multifork S P))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
replace h := Limits.IsLimit.ofIsoLimit h (S.mapMultifork F P)
no goals
case intro
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
B : Type u₃
inst✝¹ : Category B
J : GrothendieckTopology C
U : C
R : Presieve U
F : A ⥤ B
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h :
  IsLimit
    ((Cones.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj
      (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
exact ⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩