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

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

case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
⊢ firstMap P S x = secondMap P S x → Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
. intro t
  apply SecondObj.ext
  intros Y Z g f hf
  simpa [firstMap, secondMap] using t _ g hf
no goals
case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
⊢ firstMap P S x = secondMap P S x → Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
. intro t Y Z f g hf
  rw [Types.limit_ext_iff'] at t
  simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩
case mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
⊢ firstMap P S x = secondMap P S x
case mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
⊢ Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x) → firstMap P S x = secondMap P S x
intro t
case mp.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
⊢ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj f.snd.fst.op)
        { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (firstMap P S x) =
      Pi.π (fun f => P.obj f.snd.fst.op)
        { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (secondMap P S x)
case mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
⊢ firstMap P S x = secondMap P S x
apply SecondObj.ext
case mp.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ Pi.π (fun f => P.obj f.snd.fst.op)
      { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (firstMap P S x) =
    Pi.π (fun f => P.obj f.snd.fst.op)
      { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (secondMap P S x)
case mp.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
⊢ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj f.snd.fst.op)
        { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (firstMap P S x) =
      Pi.π (fun f => P.obj f.snd.fst.op)
        { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (secondMap P S x)
intros Y Z g f hf
no goals
case mp.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ Pi.π (fun f => P.obj f.snd.fst.op)
      { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (firstMap P S x) =
    Pi.π (fun f => P.obj f.snd.fst.op)
      { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } (secondMap P S x)
simpa [firstMap, secondMap] using t _ g hf
case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : firstMap P S x = secondMap P S x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) (_ : S.arrows (g ≫ f)) =
    P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)
case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
⊢ firstMap P S x = secondMap P S x → Presieve.FamilyOfElements.SieveCompatible ((firstObjEqFamily P S.arrows).hom x)
intro t Y Z f g hf
case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j (firstMap P S x) =
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j (secondMap P S x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) (_ : S.arrows (g ≫ f)) =
    P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)
case mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : FirstObj P S.arrows
t : firstMap P S x = secondMap P S x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) (_ : S.arrows (g ≫ f)) =
    P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)
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
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j (firstMap P S x) =
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j (secondMap P S x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) (_ : S.arrows (g ≫ f)) =
    P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)
simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩