C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ S ∈ GrothendieckTopology.sieves J₂ X
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
⊢ J₁ ≤ J₂
intro X S hS
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.close J₂ S = ⊤
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ S ∈ GrothendieckTopology.sieves J₂ X
rw [← J₂.close_eq_top_iff_mem]
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ GrothendieckTopology.close J₂ S = ⊤
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.close J₂ S = ⊤
have : J₂.IsClosed (⊤ : Sieve X) := by
  intro Y f _
  trivial
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this }
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ GrothendieckTopology.close J₂ S = ⊤
suffices (⟨J₂.close S, J₂.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩ by
  rw [Subtype.ext_iff] at this
  exact this
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      (Functor.closedSieves J₂).map f.op
          { val := GrothendieckTopology.close J₂ S,
            property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
        (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this }
apply (h S hS).isSeparatedFor.ext
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : GrothendieckTopology.Covers J₂ ⊤ f
⊢ ⊤.arrows f
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.IsClosed J₂ ⊤
intro Y f _
no goals
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : GrothendieckTopology.Covers J₂ ⊤ f
⊢ ⊤.arrows f
trivial
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  ↑{ val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    ↑{ val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
rw [Subtype.ext_iff] at this
no goals
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  ↑{ val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    ↑{ val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
exact this
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      (Functor.closedSieves J₂).map f.op
          { val := GrothendieckTopology.close J₂ S,
            property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
        (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
intro Y f hf
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
simp only [Functor.closedSieves_obj]
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op
        { val := GrothendieckTopology.close J₂ S,
          property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) }) =
    ↑((Functor.closedSieves J₂).map f.op { val := ⊤, property := this })
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
ext1
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₂ S) = Sieve.pullback f ⊤
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op
        { val := GrothendieckTopology.close J₂ S,
          property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) }) =
    ↑((Functor.closedSieves J₂).map f.op { val := ⊤, property := this })
dsimp
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ GrothendieckTopology.sieves J₂ Y
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₂ S) = Sieve.pullback f ⊤
rw [Sieve.pullback_top, ← J₂.pullback_close, S.pullback_eq_top_of_mem hf,
  J₂.close_eq_top_iff_mem]
no goals
case a
C : Type u
inst✝ : Category C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ GrothendieckTopology.sieves J₂ Y
apply J₂.top_mem