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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (f : functor S ⟶ P), ∃! g, functorInclusion S ≫ g = f
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
P : Cᵒᵖ ⥤ Type v₁
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S
rw [IsSheafFor, YonedaSheafCondition]
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (f : functor S ⟶ P), ∃! g, FamilyOfElements.IsAmalgamation (↑(↑natTransEquivCompatibleFamily f)) (↑yonedaEquiv g)
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (f : functor S ⟶ P), ∃! g, functorInclusion S ≫ g = f
simp_rw [extension_iff_amalgamation]
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (y : { x // FamilyOfElements.Compatible x }),
      ∃! g,
        FamilyOfElements.IsAmalgamation (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm y)))
          (↑yonedaEquiv g)
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (f : functor S ⟶ P), ∃! g, FamilyOfElements.IsAmalgamation (↑(↑natTransEquivCompatibleFamily f)) (↑yonedaEquiv g)
rw [Equiv.forall_congr_left' natTransEquivCompatibleFamily]
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (a : FamilyOfElements P S.arrows) (b : FamilyOfElements.Compatible a),
      ∃! g,
        FamilyOfElements.IsAmalgamation
          (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := a, property := b })))
          (↑yonedaEquiv g)
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (y : { x // FamilyOfElements.Compatible x }),
      ∃! g,
        FamilyOfElements.IsAmalgamation (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm y)))
          (↑yonedaEquiv g)
rw [Subtype.forall]
case H
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
P : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (x : FamilyOfElements P S.arrows) (h : FamilyOfElements.Compatible x),
    (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
      ∃! g,
        FamilyOfElements.IsAmalgamation
          (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := h })))
          (↑yonedaEquiv g)
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
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (x : FamilyOfElements P S.arrows), FamilyOfElements.Compatible x → ∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (a : FamilyOfElements P S.arrows) (b : FamilyOfElements.Compatible a),
      ∃! g,
        FamilyOfElements.IsAmalgamation
          (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := a, property := b })))
          (↑yonedaEquiv g)
apply ball_congr
case H
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
P : Cᵒᵖ ⥤ Type v₁
x : FamilyOfElements P S.arrows
hx : FamilyOfElements.Compatible x
⊢ (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∃! g,
      FamilyOfElements.IsAmalgamation
        (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := hx })))
        (↑yonedaEquiv g)
case H
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
P : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (x : FamilyOfElements P S.arrows) (h : FamilyOfElements.Compatible x),
    (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
      ∃! g,
        FamilyOfElements.IsAmalgamation
          (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := h })))
          (↑yonedaEquiv g)
intro x hx
case H
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
P : Cᵒᵖ ⥤ Type v₁
x : FamilyOfElements P S.arrows
hx : FamilyOfElements.Compatible x
⊢ (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∃! y,
      FamilyOfElements.IsAmalgamation
        (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := hx }))) y
case H
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
P : Cᵒᵖ ⥤ Type v₁
x : FamilyOfElements P S.arrows
hx : FamilyOfElements.Compatible x
⊢ (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∃! g,
      FamilyOfElements.IsAmalgamation
        (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := hx })))
        (↑yonedaEquiv g)
rw [Equiv.exists_unique_congr_left _]
no goals
case H
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
P : Cᵒᵖ ⥤ Type v₁
x : FamilyOfElements P S.arrows
hx : FamilyOfElements.Compatible x
⊢ (∃! t, FamilyOfElements.IsAmalgamation x t) ↔
    ∃! y,
      FamilyOfElements.IsAmalgamation
        (↑(↑natTransEquivCompatibleFamily (↑natTransEquivCompatibleFamily.symm { val := x, property := hx }))) y
simp