C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x) ↔ firstMap P R x = secondMap P R x
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.Compatible ((firstObjEqFamily P R).hom x) ↔ firstMap P R x = secondMap P R x
rw [Presieve.pullbackCompatible_iff]
case mp
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x) → firstMap P R x = secondMap P R x

case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x) ↔ firstMap P R x = secondMap P R x
constructor
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
case mp
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x) → firstMap P R x = secondMap P R x

case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
. intro t
  apply Limits.Types.limit_ext.{max u₁ v₁, u₁}
  rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
  simpa [firstMap, secondMap] using t hf hg
case mp
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
⊢ firstMap P R x = secondMap P R x
case mp
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x) → firstMap P R x = secondMap P R x
intro t
case mp.w
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (secondMap P R x)
case mp
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
⊢ firstMap P R x = secondMap P R x
apply Limits.Types.limit_ext.{max u₁ v₁, u₁}
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (firstMap P R x) =
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (secondMap P R x)
case mp.w
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (secondMap P R x)
rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
no goals
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (firstMap P R x) =
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
      { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
      (secondMap P R x)
simpa [firstMap, secondMap] using t hf hg
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : firstMap P R x = secondMap P R x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map pullback.fst.op ((firstObjEqFamily P R).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P R).hom x g hg)
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → Presieve.FamilyOfElements.PullbackCompatible ((firstObjEqFamily P R).hom x)
intro t Y Z f g hf hg
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (secondMap P R x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map pullback.fst.op ((firstObjEqFamily P R).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P R).hom x g hg)
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t : firstMap P R x = secondMap P R x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map pullback.fst.op ((firstObjEqFamily P R).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P R).hom x g hg)
rw [Types.limit_ext_iff'] at t
no goals
case mpr
C : Type u₁
inst✝¹ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
inst✝ : HasPullbacks C
x : FirstObj P R
t :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j (secondMap P R x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map pullback.fst.op ((firstObjEqFamily P R).hom x f hf) = P.map pullback.snd.op ((firstObjEqFamily P R).hom x g hg)
simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩