case mp
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

case mpr
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
constructor
case mp
C : Type u
inst✝ : Category C
J₁✝ J₂ J₁ : GrothendieckTopology C
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
case mp
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
rintro rfl
case mp
C : Type u
inst✝ : Category C
J₁✝ J₂ J₁ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
case mp
C : Type u
inst✝ : Category C
J₁✝ J₂ J₁ : GrothendieckTopology C
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
intro P
no goals
case mp
C : Type u
inst✝ : Category C
J₁✝ J₂ J₁ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
rfl
case mpr
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ = J₂
case mpr
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
intro h
case mpr.a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂

case mpr.a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
case mpr
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ = J₂
apply le_antisymm
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
case mpr.a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂
apply le_topology_of_closedSieves_isSheaf
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₂)
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
rw [h]
no goals
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₂)
apply classifier_isSheaf
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁)
case mpr.a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
apply le_topology_of_closedSieves_isSheaf
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁)
rw [← h]
no goals
case mpr.a.h
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
apply classifier_isSheaf