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
D : Type u₂
inst✝ : Category D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (Functor.op F ⋙ P).map g₁.op (FamilyOfElements.functorPullback F x f₁ h₁) =
    (Functor.op F ⋙ P).map g₂.op (FamilyOfElements.functorPullback F x f₂ 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
D : Type u₂
inst✝ : Category D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : Compatible x
⊢ Compatible (FamilyOfElements.functorPullback F x)
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq
no goals
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
D : Type u₂
inst✝ : Category D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (Functor.op F ⋙ P).map g₁.op (FamilyOfElements.functorPullback F x f₁ h₁) =
    (Functor.op F ⋙ P).map g₂.op (FamilyOfElements.functorPullback F x f₂ h₂)
exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])
no goals
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
D : Type u₂
inst✝ : Category D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : Compatible x
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁ ≫ F.map f₁ = F.map g₂ ≫ F.map f₂
simp only [← F.map_comp, eq]