case h.h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
          (_ :
            ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
              GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)))
        X ↔
    S ∈ GrothendieckTopology.sieves J₁ X
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
⊢ topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
      (_ :
        ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
          GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)) =
    J₁
ext (X S)
no goals
case h.h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
          (_ :
            ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
              GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)))
        X ↔
    S ∈ GrothendieckTopology.sieves J₁ X
apply GrothendieckTopology.close_eq_top_iff_mem