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 (generate R).arrows
t : FamilyOfElements.SieveCompatible x
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) = x
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 (generate R).arrows
t : FamilyOfElements.Compatible x
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) = x
rw [compatible_iff_sieveCompatible] at t
case h.h.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
x : FamilyOfElements P (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) x✝ h = x x✝ 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
x : FamilyOfElements P (generate R).arrows
t : FamilyOfElements.SieveCompatible x
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) = x
funext _ _ h
case h.h.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
x : FamilyOfElements P (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ x
      (Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
        Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝))
      (_ :
        (generate R).arrows
          (Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
            Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝))) =
    x x✝ h
case h.h.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
x : FamilyOfElements P (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x) x✝ h = x x✝ h
apply (t _ _ _).symm.trans
case h.h.h.e_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 (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
      Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝) =
    x✝
case h.h.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
x : FamilyOfElements P (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ x
      (Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
        Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝))
      (_ :
        (generate R).arrows
          (Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
            Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝))) =
    x x✝ h
congr
no goals
case h.h.h.e_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 (generate R).arrows
t : FamilyOfElements.SieveCompatible x
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫
      Exists.choose (_ : ∃ g, R g ∧ Exists.choose (_ : ∃ h_1 g, R g ∧ h_1 ≫ g = x✝) ≫ g = x✝) =
    x✝
exact h.choose_spec.choose_spec.choose_spec.2