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₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : FamilyOfElements.Compatible x₁
t₂ : FamilyOfElements.Compatible x₂
h :
  FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁) =
    FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) 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₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : FamilyOfElements.Compatible x₁
t₂ : FamilyOfElements.Compatible x₂
h :
  FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
⊢ x₁ = x₂
rw [← extend_restrict t₁, ← extend_restrict t₂]
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
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : FamilyOfElements.Compatible x₁
t₂ : FamilyOfElements.Compatible x₂
h :
  FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
⊢ FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) 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₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : FamilyOfElements.Compatible x₁
t₂ : FamilyOfElements.Compatible x₂
h :
  FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
⊢ FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁) =
    FamilyOfElements.sieveExtend (FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂)
apply congr_arg
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
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : FamilyOfElements.Compatible x₁
t₂ : FamilyOfElements.Compatible x₂
h :
  FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
⊢ FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₁ =
    FamilyOfElements.restrict (_ : R ≤ (generate R).arrows) x₂
exact h