-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem classifier_isSheaf : Presieve.IsSheaf J₁ (Functor.closedSieves J₁)

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

Tactic:
rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂

Result:
case refine_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩

Proof state:
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ Opposite.unop (Opposite.op X)
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g

Tactic:
rw [Sieve.mem_iff_pullback_eq_top, Sieve.mem_iff_pullback_eq_top, q g hg]

Result:
no goals

Proof state:
case refine_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩

Tactic:
ext Y f

Result:
case refine_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
⊢ (↑⟨M, hM⟩).arrows f ↔ (↑⟨N, hN⟩).arrows f

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₁).map f.op ⟨J₁.close M, ⋯⟩ = x f hf

Tactic:
ext1

Result:
case refine_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₁).map f.op ⟨J₁.close M, ⋯⟩) = ↑(x f hf)

Proof state:
case refine_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f M ∈ J₁ Y

Tactic:
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)

Result:
case refine_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve.pullback f (M ⊓ ?m.13254) ∈ J₁ Y

C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ Sieve X

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ Opposite.unop (Opposite.op X)
⊢ (M ⊓ S).arrows g ↔ (N ⊓ S).arrows g

Tactic:
rw [Sieve.inter_apply, Sieve.inter_apply]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ Opposite.unop (Opposite.op X)
⊢ M.arrows g ∧ S.arrows g ↔ N.arrows g ∧ S.arrows g

Proof state:
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ Opposite.unop (Opposite.op X)
⊢ S.arrows g → (M.arrows g ↔ N.arrows g)

Tactic:
intro hg

Result:
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ Opposite.unop (Opposite.op X)
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro x hx

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t