C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
⊢ IsSheaf' J P ↔ IsSheaf' J (P ⋙ s)
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)
rw [isSheaf_iff_isSheaf', isSheaf_iff_isSheaf']
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
⊢ IsSheaf' J P ↔ IsSheaf' J (P ⋙ s)
refine' forall_congr' (fun U => ball_congr (fun R _ => _))
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
letI : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
have : IsLimit (s.mapCone (Fork.ofι _ (w R P))) ≃ IsLimit (Fork.ofι _ (w R (P ⋙ s))) :=
  isSheafForIsSheafFor' P s U R
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R 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✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap R (P ⋙ s))
          (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s))))
rw [← Equiv.nonempty_congr this]
case mp
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) →
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))))

case mpr
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))) →
    Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R 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✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ↔
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))))
constructor
case mp
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝¹ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this✝ :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
this : PreservesLimitsOfSize s
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) →
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))))
case mp
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) →
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))))
haveI := preservesSmallestLimitsOfPreservesLimits s
no goals
case mp
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝¹ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this✝ :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
this : PreservesLimitsOfSize s
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) →
    Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))))
exact Nonempty.map fun t => isLimitOfPreserves s t
case mpr
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝¹ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this✝ :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
this : ReflectsLimitsOfSize s
⊢ Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))) →
    Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
case mpr
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
⊢ Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))) →
    Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
haveI := reflectsSmallestLimitsOfReflectsLimits s
no goals
case mpr
C : Type u₁
inst✝⁵ : Category C
A : Type u₂
inst✝⁴ : Category A
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P : Cᵒᵖ ⥤ A
inst✝³ : HasPullbacks C
s : A ⥤ Type (max v₁ u₁)
inst✝² : HasLimits A
inst✝¹ : PreservesLimits s
inst✝ : ReflectsIsomorphisms s
U : C
R : Presieve U
x✝ : generate R ∈ GrothendieckTopology.sieves J U
this✝¹ : ReflectsLimits s := reflectsLimitsOfReflectsIsomorphisms
this✝ :
  IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P))) ≃
    IsLimit
      (Fork.ofι (forkMap R (P ⋙ s))
        (_ : forkMap R (P ⋙ s) ≫ firstMap R (P ⋙ s) = forkMap R (P ⋙ s) ≫ secondMap R (P ⋙ s)))
this : ReflectsLimitsOfSize s
⊢ Nonempty
      (IsLimit (s.mapCone (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))) →
    Nonempty (IsLimit (Fork.ofι (forkMap R P) (_ : forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P)))
exact Nonempty.map fun t => isLimitOfReflects s t