C : Type u_1
inst✝³ : Category C
D : Type u_3
inst✝² : Category D
E : Type ?u.5750
inst✝¹ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.5802
inst✝ : Category A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj X.op
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
C : Type u_1
inst✝³ : Category C
D : Type u_3
inst✝² : Category D
E : Type ?u.5750
inst✝¹ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.5802
inst✝ : Category A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj X.op
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ s = t
apply (ℱ.cond (Sieve.coverByImage G X) (H.is_cover X)).isSeparatedFor.ext
case intro.mk.refl
C : Type u_1
inst✝³ : Category C
D : Type u_3
inst✝² : Category D
E : Type ?u.5750
inst✝¹ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.5802
inst✝ : Category A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj X.op
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ ℱ.val.map (f₁ ≫ f₂).op s = ℱ.val.map (f₁ ≫ f₂).op t
C : Type u_1
inst✝³ : Category C
D : Type u_3
inst✝² : Category D
E : Type ?u.5750
inst✝¹ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.5802
inst✝ : Category A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj X.op
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ X⦄, (Sieve.coverByImage G X).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
rintro Y _ ⟨Z, f₁, f₂, ⟨rfl⟩⟩
no goals
case intro.mk.refl
C : Type u_1
inst✝³ : Category C
D : Type u_3
inst✝² : Category D
E : Type ?u.5750
inst✝¹ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.5802
inst✝ : Category A
G : C ⥤ D
H✝ H : CoverDense K G
ℱ : SheafOfTypes K
X : D
s t : ℱ.val.obj X.op
h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t
Y : D
Z : C
f₁ : Y ⟶ G.obj Z
f₂ : G.obj Z ⟶ X
⊢ ℱ.val.map (f₁ ≫ f₂).op s = ℱ.val.map (f₁ ≫ f₂).op t
simp [h f₂]