C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁) S.arrows
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
intro X S hS
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁) S.arrows
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
case refine'_1
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows

case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
    Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
refine' ⟨_, _⟩
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
case refine'_1
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows
rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
simp only [Functor.closedSieves_obj]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
⊢ ∀ (f : Y ⟶ X.op.unop), (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
case refine'_1.mk.mk
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
ext Y
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
⊢ ∀ (f : Y ⟶ X.op.unop), (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
intro f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ M.arrows f ↔ N.arrows f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
dsimp only [Subtype.coe_mk]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ M.arrows f ↔ N.arrows f
rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
have q : ∀ ⦃Z : C⦄ (g : Z ⟶ X) (_ : S g), M.pullback g = N.pullback g :=
  fun Z g hg => congr_arg Subtype.val ((hM₂ g hg).trans (hN₂ g hg).symm)
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
have MSNS : M ⊓ S = N ⊓ S := by
  ext Z
  intro g
  rw [Sieve.inter_apply, Sieve.inter_apply]
  simp only [and_comm]
  apply and_congr_right
  intro hg
  rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f → GrothendieckTopology.Covers J₁ N f

case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ N f → GrothendieckTopology.Covers J₁ M f
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
constructor
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
⊢ ∀ (f : Z ⟶ X.op.unop), (M ⊓ S).arrows f ↔ (N ⊓ S).arrows f
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ M ⊓ S = N ⊓ S
ext Z
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ (M ⊓ S).arrows g ↔ (N ⊓ S).arrows g
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
⊢ ∀ (f : Z ⟶ X.op.unop), (M ⊓ S).arrows f ↔ (N ⊓ S).arrows f
intro g
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ M.arrows g ∧ S.arrows g ↔ N.arrows g ∧ S.arrows g
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ (M ⊓ S).arrows g ↔ (N ⊓ S).arrows g
rw [Sieve.inter_apply, Sieve.inter_apply]
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ S.arrows g ∧ M.arrows g ↔ S.arrows g ∧ N.arrows g
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ M.arrows g ∧ S.arrows g ↔ N.arrows g ∧ S.arrows g
simp only [and_comm]
case h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ S.arrows g → (M.arrows g ↔ N.arrows g)
case h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ S.arrows g ∧ M.arrows g ↔ S.arrows g ∧ N.arrows g
apply and_congr_right
case h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g
case h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
⊢ S.arrows g → (M.arrows g ↔ N.arrows g)
intro hg
no goals
case h.h
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ X.op.unop
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g
rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ GrothendieckTopology.Covers J₁ N f
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f → GrothendieckTopology.Covers J₁ N f
intro hf
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f N ∈ GrothendieckTopology.sieves J₁ Y
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ GrothendieckTopology.Covers J₁ N f
rw [J₁.covers_iff]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (N ⊓ ?m.20451) ∈ GrothendieckTopology.sieves J₁ Y

C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve X.op.unop
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f N ∈ GrothendieckTopology.sieves J₁ Y
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (M ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (N ⊓ ?m.20451) ∈ GrothendieckTopology.sieves J₁ Y

C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve X.op.unop
rw [← MSNS]
no goals
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (M ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ GrothendieckTopology.Covers J₁ M f
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ N f → GrothendieckTopology.Covers J₁ M f
intro hf
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f M ∈ GrothendieckTopology.sieves J₁ Y
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ GrothendieckTopology.Covers J₁ M f
rw [J₁.covers_iff]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (M ⊓ ?m.20658) ∈ GrothendieckTopology.sieves J₁ Y

C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve X.op.unop
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f M ∈ GrothendieckTopology.sieves J₁ Y
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (N ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (M ⊓ ?m.20658) ∈ GrothendieckTopology.sieves J₁ Y

C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve X.op.unop
rw [MSNS]
no goals
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve X.op.unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve X.op.unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ X.op.unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (N ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
apply J₁.arrow_intersect f N S hf (J₁.pullback_stable _ hS)
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
    Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
intro x hx
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
rw [Presieve.compatible_iff_sieveCompatible] at hx
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
let M := Sieve.bind S fun Y f hf => (x f hf).1
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
⊢ Presieve.FamilyOfElements.IsAmalgamation x
    { val := GrothendieckTopology.close J₁ M,
      property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
refine' ⟨⟨_, J₁.close_isClosed M⟩, _⟩
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
intro Y f hf
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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 C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
apply le_antisymm
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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) (_ : S.arrows (u ≫ f))) = ⊤
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
rw [Sieve.pullback_eq_top_iff_mem,
  ← show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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 (g ≫ f') (_ : S.arrows (g ≫ f'))) = ⊤
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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) (_ : S.arrows (u ≫ f))) = ⊤
conv_lhs => congr; congr; rw [← c]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
⊢ ↑((Functor.closedSieves J₁).map g.op (x f' hf')) = ⊤
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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 (g ≫ f') (_ : S.arrows (g ≫ f'))) = ⊤
rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
no goals
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
⊢ ↑((Functor.closedSieves J₁).map g.op (x f' hf')) = ⊤
apply Sieve.pullback_eq_top_of_mem _ hg
no goals
case a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
      { val := GrothendieckTopology.close J₁ M,
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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)
⊢ Presieve.FamilyOfElements.IsAmalgamation x
    { val := GrothendieckTopology.close J₁ M,
      property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }
intro Y f hf
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
      { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
      { val := GrothendieckTopology.close J₁ M,
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
simp only [Functor.closedSieves_obj]
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
        { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
          property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }) =
    ↑(x f hf)
case refine'_2
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
      { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
ext1
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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 (GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf))) = ↑(x f hf)
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
        { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
          property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }) =
    ↑(x f hf)
dsimp
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
⊢ GrothendieckTopology.close J₁ ↑(x f hf) = ↑(x f hf)
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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 (GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf))) = ↑(x f hf)
rw [← J₁.pullback_close, this _ hf]
no goals
case refine'_2.a
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
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
⊢ GrothendieckTopology.close J₁ ↑(x f hf) = ↑(x f hf)
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)