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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ FamilyOfElements.sieveExtend x f (_ : f ∈ (generate R).arrows) = 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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.sieveExtend x f (_ : f ∈ (generate R).arrows) = x f hf
have h := (le_generate R Y hf).choose_spec
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ 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)))) =
    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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ FamilyOfElements.sieveExtend x f (_ : f ∈ (generate R).arrows) = x f hf
unfold FamilyOfElements.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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map (𝟙 Y).op (x f hf) = 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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ Exists.choose h ≫ Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f) = 𝟙 Y ≫ 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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ 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)))) =
    x f hf
rw [t h.choose (𝟙 _) _ hf _]
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ P.map (𝟙 Y).op (x f hf) = x f hf
simp
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ Exists.choose h ≫ Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f) = 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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ Exists.choose h ≫ Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f) = 𝟙 Y ≫ f
rw [id_comp]
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
x : FamilyOfElements P R
t : FamilyOfElements.Compatible x
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ Exists.choose h ≫ Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h g, R g ∧ h ≫ g = f) ≫ g = f) = f
exact h.choose_spec.choose_spec.2