-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem le_topology_of_closedSieves_isSheaf {J₁ J₂ : GrothendieckTopology C}
    (h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)) : J₁ ≤ J₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → (Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩ = (Functor.closedSieves J₂).map f.op ⟨⊤, this⟩

Tactic:
intro Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩ = (Functor.closedSieves J₂).map f.op ⟨⊤, this⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ J₂.close S = ⊤

Tactic:
have : J₂.IsClosed (⊤ : Sieve X) := by
  intro Y f _
  trivial

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ J₂.close S = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ ⟨J₂.close S, ⋯⟩ = ⟨⊤, this⟩

Tactic:
apply (h S hS).isSeparatedFor.ext

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → (Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩ = (Functor.closedSieves J₂).map f.op ⟨⊤, this⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this✝ : J₂.IsClosed ⊤
this : ⟨J₂.close S, ⋯⟩ = ⟨⊤, this✝⟩
⊢ J₂.close S = ⊤

Tactic:
rw [Subtype.ext_iff] at this

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this✝ : J₂.IsClosed ⊤
this : ↑⟨J₂.close S, ⋯⟩ = ↑⟨⊤, this✝⟩
⊢ J₂.close S = ⊤

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (J₂.close S) = Sieve.pullback f ⊤

Tactic:
rw [Sieve.pullback_top, ← J₂.pullback_close, S.pullback_eq_top_of_mem hf,
  J₂.close_eq_top_iff_mem]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ J₂ Y

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ J₂ Y

Tactic:
apply J₂.top_mem

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩ = (Functor.closedSieves J₂).map f.op ⟨⊤, this⟩

Tactic:
ext1

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩) = ↑((Functor.closedSieves J₂).map f.op ⟨⊤, this⟩)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ S ∈ J₂ X

Tactic:
rw [← J₂.close_eq_top_iff_mem]

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ J₂.close S = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
Y : C
f : Y ⟶ X
a✝ : J₂.Covers ⊤ f
⊢ ⊤.arrows f

Tactic:
trivial

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ J₂.IsClosed ⊤

Tactic:
intro Y f _

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
Y : C
f : Y ⟶ X
a✝ : J₂.Covers ⊤ f
⊢ ⊤.arrows f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this✝ : J₂.IsClosed ⊤
this : ↑⟨J₂.close S, ⋯⟩ = ↑⟨⊤, this✝⟩
⊢ J₂.close S = ⊤

Tactic:
exact this

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ J₂.close S = ⊤

Tactic:
suffices (⟨J₂.close S, J₂.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩ by
  rw [Subtype.ext_iff] at this
  exact this

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
⊢ ⟨J₂.close S, ⋯⟩ = ⟨⊤, this⟩

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op ⟨J₂.close S, ⋯⟩) = ↑((Functor.closedSieves J₂).map f.op ⟨⊤, this⟩)

Tactic:
dsimp

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
this : J₂.IsClosed ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (J₂.close S) = Sieve.pullback f ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
⊢ J₁ ≤ J₂

Tactic:
intro X S hS

Result:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ S ∈ J₂ X