case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))) →
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows

case mpr
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))) ↔
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
constructor
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
⊢ t₁ = t₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))) →
    ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
intro hs E x t₁ t₂ h₁ h₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : Compatible x
⊢ t₁ = t₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
⊢ t₁ = t₂
have hx := is_compatible_of_exists_amalgamation x ⟨t₁, h₁⟩
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
⊢ t₁ = t₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : Compatible x
⊢ t₁ = t₂
rw [compatible_iff_sieveCompatible] at hx
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
hs : Subsingleton (SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
⊢ t₁ = t₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
hs : ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
⊢ t₁ = t₂
specialize hs hx.cone
case mp.intro
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
hs : ∀ (a b : SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
⊢ t₁ = t₂
case mp
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
hs : Subsingleton (SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
⊢ t₁ = t₂
rcases hs with ⟨hs⟩
no goals
case mp.intro
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x✝ : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx✝ : SieveCompatible x✝
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj X.op
h₁ : IsAmalgamation x t₁
h₂ : IsAmalgamation x t₂
hx : SieveCompatible x
hs : ∀ (a b : SieveCompatible.cone hx ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
⊢ t₁ = t₂
simpa only [Subtype.mk.injEq] using (show Subtype.mk t₁ h₁ = ⟨t₂, h₂⟩ from
  (homEquivAmalgamation hx).symm.injective (hs _ _))
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
case mpr
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : SieveCompatible x
⊢ (∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows) →
    ∀ (c : Cone (Functor.op (diagram S.arrows) ⋙ P)), Subsingleton (c ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
rintro h ⟨E, π⟩
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
let eqv := conesEquivSieveCompatibleFamily P S (op E)
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∀ (a b : { pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
case mpr.mk
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ Subsingleton ({ pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows)))
constructor
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∀ (a b : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∀ (a b : { pt := E, π := π } ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
rw [← eqv.left_inv π]
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
⊢ f₁ = f₂
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
⊢ ∀ (a b : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))), a = b
intro f₁ f₂
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ f₁ = f₂
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
⊢ f₁ = f₂
let eqv' := homEquivAmalgamation (eqv π).2
case mpr.mk.allEq.a
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ ↑eqv' f₁ = ↑eqv' f₂
case mpr.mk.allEq
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ f₁ = f₂
apply eqv'.injective
case mpr.mk.allEq.a.a
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ ↑(↑eqv' f₁) = ↑(↑eqv' f₂)
case mpr.mk.allEq.a
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ ↑eqv' f₁ = ↑eqv' f₂
ext
no goals
case mpr.mk.allEq.a.a
C : Type u₁
inst✝¹ : Category C
A : Type u₂
inst✝ : Category A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E✝ : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E✝) S.arrows
hx : SieveCompatible x
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const (FullSubcategory fun f => S.arrows f.hom)ᵒᵖ).obj E ⟶ Functor.op (diagram S.arrows) ⋙ P
eqv : (Functor.cones (Functor.op (diagram S.arrows) ⋙ P)).obj E.op ≃ { x // SieveCompatible x } :=
  conesEquivSieveCompatibleFamily P S E.op
f₁ f₂ : { pt := E, π := Equiv.invFun eqv (Equiv.toFun eqv π) } ⟶ P.mapCone (Cocone.op (cocone S.arrows))
eqv' : (SieveCompatible.cone (_ : SieveCompatible ↑(↑eqv π)) ⟶ P.mapCone (Cocone.op (cocone S.arrows))) ≃
  { t // IsAmalgamation (↑(↑eqv π)) t } :=
  homEquivAmalgamation (_ : SieveCompatible ↑(↑eqv π))
⊢ ↑(↑eqv' f₁) = ↑(↑eqv' f₂)
apply h _ (eqv π).1 <;> exact (eqv' _).2