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

Proof state:
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)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M = ↑(x f hf)

Tactic:
apply le_antisymm

Result:
case 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)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M ≤ ↑(x f hf)

case 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)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M

Proof state:
case a.intro.intro.intro.intro.intro
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)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ (↑(x f hf)).arrows u

Tactic:
rw [Sieve.mem_iff_pullback_eq_top,
  ← show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]

Result:
case a.intro.intro.intro.intro.intro
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)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (u ≫ f) ⋯) = ⊤

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 ⊓ ?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

Tactic:
rw [MSNS]

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 (N ⊓ S) ∈ J₁ Y

Proof state:
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
⊢ J₁.close ↑(x f hf) = ↑(x f hf)

Tactic:
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)

Result:
no goals

Proof state:
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
⊢ Sieve.pullback f (J₁.close M) = ↑(x f hf)

Tactic:
rw [← J₁.pullback_close, this _ hf]

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
⊢ J₁.close ↑(x f hf) = ↑(x f hf)

Proof state:
case refine_1.mk.mk.a.h.mp
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
⊢ J₁.Covers M f → J₁.Covers N f

Tactic:
intro hf

Result:
case refine_1.mk.mk.a.h.mp
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 M f
⊢ J₁.Covers N 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
⊢ ∃ t, x.IsAmalgamation t

Tactic:
let M := Sieve.bind S fun Y f hf => (x f hf).1

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.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∃ t, x.IsAmalgamation t

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.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
rw [Presieve.compatible_iff_sieveCompatible] at 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.SieveCompatible
⊢ ∃ t, x.IsAmalgamation t

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

Tactic:
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Result:
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 ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t