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
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = FamilyOfElements.sieveExtend x f hf
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
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
⊢ FamilyOfElements.IsAmalgamation (FamilyOfElements.sieveExtend x) t
intro Y f hf
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
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t =
    P.map (Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f)).op
      (x (Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f))
        (_ : R (Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ 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
R : Presieve X
x : FamilyOfElements P R
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = FamilyOfElements.sieveExtend x f hf
dsimp [FamilyOfElements.sieveExtend]
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
x : FamilyOfElements P R
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t =
    P.map (Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f)).op
      (x (Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f))
        (_ : R (Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f))))
rw [← ht _, ← FunctorToTypes.map_comp_apply, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]