C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
⊢ SieveCompatible (FamilyOfElements.pullback f x)
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : Compatible x
⊢ Compatible (FamilyOfElements.pullback f x)
simp only [compatible_iff_sieveCompatible] at h ⊢
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) =
    P.map f₂.op (FamilyOfElements.pullback f x f₁ hf)
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
⊢ SieveCompatible (FamilyOfElements.pullback f x)
intro W Z f₁ f₂ hf
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) = P.map f₂.op (x (f₁ ≫ f) hf)
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) =
    P.map f₂.op (FamilyOfElements.pullback f x f₁ hf)
unfold FamilyOfElements.pullback
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) = x (f₂ ≫ f₁ ≫ f) (_ : S.arrows (f₂ ≫ f₁ ≫ f))
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) = P.map f₂.op (x (f₁ ≫ f) hf)
rw [← h (f₁ ≫ f) f₂ hf]
case e_f
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) (_ : (Sieve.pullback f S).arrows (f₂ ≫ f₁)) = x (f₂ ≫ f₁ ≫ f) (_ : S.arrows (f₂ ≫ f₁ ≫ f))
congr 1
no goals
case e_f
C : Type u₁
inst✝ : Category C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
J J₂ : GrothendieckTopology C
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : SieveCompatible x
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ (f₂ ≫ f₁) ≫ f = f₂ ≫ f₁ ≫ f
simp only [assoc]