case refine'_1
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y

case refine'_2
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)
refine' @IsGLB.of_image _ _ _ _ sieves _ _ _ _
case refine'_1
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
x✝ y✝ : GrothendieckTopology C
⊢ x✝.sieves ≤ y✝.sieves ↔ x✝ ≤ y✝
case refine'_1
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y
intros
no goals
case refine'_1
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
x✝ y✝ : GrothendieckTopology C
⊢ x✝.sieves ≤ y✝.sieves ↔ x✝ ≤ y✝
rfl
no goals
case refine'_2
C : Type u
inst✝ : Category C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves
exact _root_.isGLB_sInf _