C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      firstMap P S (↑(firstObjEqFamily P S.arrows).symm x) = secondMap P S (↑(firstObjEqFamily P S.arrows).symm x) →
        ∃! x_1, forkMap P S.arrows x_1 = ↑(firstObjEqFamily P S.arrows).symm x
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    Nonempty
      (IsLimit
        (Fork.ofι (forkMap P S.arrows) (_ : forkMap P S.arrows ≫ firstMap P S = forkMap P S.arrows ≫ secondMap P S)))
rw [Types.type_equalizer_iff_unique,
  ← Equiv.forall_congr_left (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible ((firstObjEqFamily P S.arrows).hom (↑(firstObjEqFamily P S.arrows).symm x)) →
        ∃! x_1, forkMap P S.arrows x_1 = ↑(firstObjEqFamily P S.arrows).symm x
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      firstMap P S (↑(firstObjEqFamily P S.arrows).symm x) = secondMap P S (↑(firstObjEqFamily P S.arrows).symm x) →
        ∃! x_1, forkMap P S.arrows x_1 = ↑(firstObjEqFamily P S.arrows).symm x
simp_rw [← compatible_iff]
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible ((firstObjEqFamily P S.arrows).hom (↑(firstObjEqFamily P S.arrows).symm x)) →
        ∃! x_1, forkMap P S.arrows x_1 = ↑(firstObjEqFamily P S.arrows).symm x
simp only [inv_hom_id_apply, Iso.toEquiv_symm_fun]
case H
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ ∀ (x : Presieve.FamilyOfElements P S.arrows),
    Presieve.FamilyOfElements.Compatible x →
      ((∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
        ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x)
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (x : Presieve.FamilyOfElements P S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x
apply ball_congr
case H
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ (∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
    ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x
case H
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ ∀ (x : Presieve.FamilyOfElements P S.arrows),
    Presieve.FamilyOfElements.Compatible x →
      ((∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
        ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x)
intro x _
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    Presieve.FamilyOfElements.IsAmalgamation x a ↔ forkMap P S.arrows a = (firstObjEqFamily P S.arrows).inv x
case H
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ (∃! t, Presieve.FamilyOfElements.IsAmalgamation x t) ↔
    ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x
apply exists_unique_congr
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P S.arrows t = (firstObjEqFamily P S.arrows).inv x
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    Presieve.FamilyOfElements.IsAmalgamation x a ↔ forkMap P S.arrows a = (firstObjEqFamily P S.arrows).inv x
intro t
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P S.arrows t = ↑(firstObjEqFamily P S.arrows).symm x
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P S.arrows t = (firstObjEqFamily P S.arrows).inv x
rw [← Iso.toEquiv_symm_fun]
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ forkMap P S.arrows t = ↑(firstObjEqFamily P S.arrows).symm x
rw [Equiv.eq_symm_apply]
case H.h.mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t → ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x

case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
case H.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t ↔ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
constructor
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
case H.h.mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t → ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x

case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
. intro q
  funext Y f hf
  simpa [firstObjEqFamily, forkMap] using q _ _
case H.h.mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
case H.h.mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ Presieve.FamilyOfElements.IsAmalgamation x t → ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
intro q
case H.h.mp.h.h.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf = x f hf
case H.h.mp
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
funext Y f hf
no goals
case H.h.mp.h.h.h
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : Presieve.FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf = x f hf
simpa [firstObjEqFamily, forkMap] using q _ _
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = x f hf
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
⊢ ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x → Presieve.FamilyOfElements.IsAmalgamation x t
intro q Y f hf
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = x f hf
rw [← q]
no goals
case H.h.mpr
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
h✝ : Presieve.FamilyOfElements.Compatible x
t : P.obj X.op
q : ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ P.map f.op t = ↑(firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) f hf
simp [firstObjEqFamily, forkMap]