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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSheafFor P (generate R).arrows
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
R : Presieve X
⊢ IsSheafFor P R ↔ IsSheafFor P (generate R).arrows
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSheafFor P (generate R).arrows
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
rw [← isSeparatedFor_iff_generate]
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
apply and_congr (Iff.refl _)
case mp
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) →
    ∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t

case mpr
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) →
    ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
constructor
case mp
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
case mp
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) →
    ∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
intro q x hx
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    FamilyOfElements.IsAmalgamation (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) a →
      FamilyOfElements.IsAmalgamation x a
case mp
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
apply Exists.imp _ (q _ (hx.restrict (le_generate R)))
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) t
⊢ FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    FamilyOfElements.IsAmalgamation (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) a →
      FamilyOfElements.IsAmalgamation x a
intro t ht
no goals
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
R : Presieve X
q : ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P (generate R).arrows
hx : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) t
⊢ FamilyOfElements.IsAmalgamation x t
simpa [hx] using isAmalgamation_sieveExtend _ _ ht
case mpr
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
case mpr
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
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows),
      FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t) →
    ∀ (x : FamilyOfElements P R), FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
intro q x hx
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    FamilyOfElements.IsAmalgamation (FamilyOfElements.sieveExtend x) a → FamilyOfElements.IsAmalgamation x a
case mpr
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
⊢ ∃ t, FamilyOfElements.IsAmalgamation x t
apply Exists.imp _ (q _ hx.sieveExtend)
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation (FamilyOfElements.sieveExtend x) t
⊢ FamilyOfElements.IsAmalgamation x t
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
⊢ ∀ (a : P.obj X.op),
    FamilyOfElements.IsAmalgamation (FamilyOfElements.sieveExtend x) a → FamilyOfElements.IsAmalgamation x a
intro t ht
no goals
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
R : Presieve X
q :
  ∀ (x : FamilyOfElements P (generate R).arrows),
    FamilyOfElements.Compatible x → ∃ t, FamilyOfElements.IsAmalgamation x t
x : FamilyOfElements P R
hx : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation (FamilyOfElements.sieveExtend x) t
⊢ FamilyOfElements.IsAmalgamation x t
simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht