case mp
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
⊢ FamilyOfElements.Compatible x → FamilyOfElements.PullbackCompatible x

case mpr
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
⊢ FamilyOfElements.PullbackCompatible x → FamilyOfElements.Compatible 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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
⊢ FamilyOfElements.Compatible x ↔ FamilyOfElements.PullbackCompatible x
constructor
case mp
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)
case mp
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
⊢ FamilyOfElements.Compatible x → FamilyOfElements.PullbackCompatible x
intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂
case mp.a
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
case mp
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ P.map pullback.fst.op (x f₁ hf₁) = P.map pullback.snd.op (x f₂ hf₂)
apply t
no goals
case mp.a
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.Compatible x
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ pullback.fst ≫ f₁ = pullback.snd ≫ f₂
apply pullback.condition
case mpr
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.PullbackCompatible x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
case mpr
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
⊢ FamilyOfElements.PullbackCompatible x → FamilyOfElements.Compatible x
intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
no goals
case mpr
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
x : FamilyOfElements P R
inst✝ : HasPullbacks C
t : FamilyOfElements.PullbackCompatible x
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]