[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
⊢ S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X →
    Sieve.pullback g S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
[PROOFSTEP]
rintro ⟨R, hR, RS⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.pullback g S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
[PROOFSTEP]
refine' ⟨_, K.pullbacks g _ hR, _⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ pullbackArrows g R ≤ (Sieve.pullback g S).arrows
[PROOFSTEP]
rw [← Sieve.sets_iff_generate, Sieve.pullbackArrows_comm]
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.pullback g (Sieve.generate R) ≤ Sieve.pullback g S
[PROOFSTEP]
apply Sieve.pullback_monotone
[GOAL]
case intro.intro.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S
[PROOFSTEP]
rwa [Sieve.giGenerate.gc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y) →
          R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
rintro X S ⟨R', hR', RS⟩ R t
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) Y
⊢ R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
choose t₁ t₂ t₃ using t
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
⊢ R ∈ (fun X S => ∃ R, R ∈ coverings K X ∧ R ≤ S.arrows) X
[PROOFSTEP]
refine' ⟨_, K.Transitive _ _ hR' fun _ f hf => t₂ (RS _ hf), _⟩
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
⊢ (Presieve.bind R' fun x f hf => t₁ (_ : f ∈ S.arrows)) ≤ R.arrows
[PROOFSTEP]
rintro Y _ ⟨Z, g, f, hg, hf, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
S : Sieve X
R' : Presieve X
hR' : R' ∈ coverings K X
RS : R' ≤ S.arrows
R : Sieve X
t₁ : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → Presieve Y
t₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ∈ coverings K Y
t₃ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : S.arrows f), t₁ a ≤ (Sieve.pullback f R).arrows
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hg : R' f
hf : t₁ (_ : f ∈ S.arrows) g
⊢ g ≫ f ∈ R.arrows
[PROOFSTEP]
apply t₃ (RS _ hg) _ hf
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
i : IsIso f
⊢ Sieve.generate (Presieve.singleton f) = ⊤
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
⊢ pullbackArrows f R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
[PROOFSTEP]
simp only [Set.mem_def, Sieve.pullbackArrows_comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
⊢ GrothendieckTopology.sieves J Y (Sieve.pullback f (Sieve.generate R))
[PROOFSTEP]
apply J.pullback_stable f hR
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
⊢ Presieve.bind S Ti ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
[PROOFSTEP]
apply J.transitive hS
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    (Sieve.generate S).arrows f →
      Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
intro Y f
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y : C
f : Y ⟶ X
⊢ (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
rintro ⟨Z, g, f, hf, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
rw [Sieve.pullback_comp]
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))) ∈ GrothendieckTopology.sieves J Y
[PROOFSTEP]
apply J.pullback_stable g
[GOAL]
case h.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback f (Sieve.generate (Presieve.bind S Ti)) ∈ GrothendieckTopology.sieves J Z
[PROOFSTEP]
apply J.superset_covering _ (hTi _ hf)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))
[PROOFSTEP]
rintro Y g ⟨W, h, g, hg, rfl⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ (Sieve.pullback f (Sieve.generate (Presieve.bind S Ti))).arrows (h ≫ g)
[PROOFSTEP]
exact ⟨_, h, _, ⟨_, _, _, hf, hg, rfl⟩, by simp⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X R => Sieve.generate R ∈ GrothendieckTopology.sieves J X) Y
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J ↔ K ≤ ofGrothendieck C J
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ toGrothendieck C K ≤ J → K ≤ ofGrothendieck C J
[PROOFSTEP]
intro h X R hR
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : toGrothendieck C K ≤ J
X : C
R : Presieve X
hR : R ∈ coverings K X
⊢ R ∈ coverings (ofGrothendieck C J) X
[PROOFSTEP]
exact h _ ⟨_, hR, Sieve.le_generate R⟩
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K ≤ ofGrothendieck C J → toGrothendieck C K ≤ J
[PROOFSTEP]
rintro h X S ⟨R, hR, RS⟩
[GOAL]
case mpr.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K ≤ ofGrothendieck C J
X : C
S : Sieve X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ S ∈ GrothendieckTopology.sieves J X
[PROOFSTEP]
apply J.superset_covering _ (h _ hR)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K ≤ ofGrothendieck C J
X : C
S : Sieve X
R : Presieve X
hR : R ∈ coverings K X
RS : R ≤ S.arrows
⊢ Sieve.generate R ≤ S
[PROOFSTEP]
rwa [Sieve.giGenerate.gc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X →
    pullbackArrows f S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
[PROOFSTEP]
rintro ⟨Z, g, i, rfl⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
[PROOFSTEP]
refine' ⟨pullback g f, pullback.snd, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso pullback.snd
[PROOFSTEP]
refine' ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨_, by aesop_cat⟩⟩⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (f ≫ inv g) ≫ g = 𝟙 Y ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f) ≫ pullback.snd = 𝟙 Y
[PROOFSTEP]
aesop_cat
[GOAL]
case intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f) = 𝟙 (pullback g f)
[PROOFSTEP]
ext
[GOAL]
case intro.intro.intro.refine'_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f)) ≫ pullback.fst =
    𝟙 (pullback g f) ≫ pullback.fst
[PROOFSTEP]
rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
[GOAL]
case intro.intro.intro.refine'_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.fst ≫ g ≫ inv g = 𝟙 (pullback g f) ≫ pullback.fst
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.refine'_1.h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd ≫ pullback.lift (f ≫ inv g) (𝟙 Y) (_ : (f ≫ inv g) ≫ g = 𝟙 Y ≫ f)) ≫ pullback.snd =
    𝟙 (pullback g f) ≫ pullback.snd
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullbackArrows f (Presieve.singleton g) = Presieve.singleton pullback.snd
[PROOFSTEP]
apply pullback_singleton
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
⊢ ∀ ⦃X : C⦄ (S : Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y),
    S ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X →
      (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y) →
        Presieve.bind S Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
rintro X S Ti ⟨Z, g, i, rfl⟩ hS
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
⊢ Presieve.bind (Presieve.singleton g) Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ Presieve.bind (Presieve.singleton g) Ti ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) X
[PROOFSTEP]
refine' ⟨_, f ≫ g, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ IsIso (f ≫ g)
[PROOFSTEP]
infer_instance
  -- Porting note: the next four lines were just "ext (W k)"
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply funext
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
⊢ ∀ (x : C), Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro W
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
⊢ Presieve.bind (Presieve.singleton g) Ti = Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply Set.ext
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
⊢ ∀ (x : W ⟶ X), x ∈ Presieve.bind (Presieve.singleton g) Ti ↔ x ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro k
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.bind (Presieve.singleton g) Ti ↔ k ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.bind (Presieve.singleton g) Ti → k ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rintro ⟨V, h, k, ⟨_⟩, hh, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Ti g (_ : singleton' g g) h
⊢ h ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
rw [hTi] at hh 
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Presieve.singleton f h
⊢ h ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
cases hh
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mp.intro.intro.intro.intro.mk.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ f ≫ g ∈ Presieve.singleton (f ≫ g)
[PROOFSTEP]
apply singleton.mk
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
W : C
k : W ⟶ X
⊢ k ∈ Presieve.singleton (f ≫ g) → k ∈ Presieve.bind (Presieve.singleton g) Ti
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ f ≫ g ∈ Presieve.bind (Presieve.singleton g) Ti
[PROOFSTEP]
refine' bind_comp g singleton.mk _
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ Ti g (_ : Presieve.singleton g g) f
[PROOFSTEP]
rw [hTi]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.h.h.mpr.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ (fun X S => ∃ Y f x, S = Presieve.singleton f) Y
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g (_ : Presieve.singleton g g) = Presieve.singleton f
Y : C
⊢ Presieve.singleton f f
[PROOFSTEP]
apply singleton.mk
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
R : Presieve X
⊢ R ∈ coverings ⊥ X → R ∈ coverings K X
[PROOFSTEP]
rintro ⟨Y, f, hf, rfl⟩
[GOAL]
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
f : Y ⟶ X
hf : IsIso f
⊢ Presieve.singleton f ∈ coverings K X
[PROOFSTEP]
exact K.has_isos f
