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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
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
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))
intro x _
case refine'_1
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X)))

case refine'_2
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ ∀ (y : P.obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = x (𝟙 X) (_ : singleton (𝟙 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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ ∃! t, FamilyOfElements.IsAmalgamation x t
refine' ⟨x _ (Presieve.singleton_self _), _, _⟩
case refine'_1.mk
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
Y : C
⊢ P.map (𝟙 X).op (x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X))) = x (𝟙 X) (_ : singleton' (𝟙 X) (𝟙 X))
case refine'_1
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ (fun t => FamilyOfElements.IsAmalgamation x t) (x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X)))
rintro _ _ ⟨rfl, rfl⟩
no goals
case refine'_1.mk
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
Y : C
⊢ P.map (𝟙 X).op (x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X))) = x (𝟙 X) (_ : singleton' (𝟙 X) (𝟙 X))
simp
case refine'_2
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
⊢ t = x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X))
case refine'_2
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
⊢ ∀ (y : P.obj X.op), (fun t => FamilyOfElements.IsAmalgamation x t) y → y = x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X))
intro t ht
no goals
case refine'_2
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : FamilyOfElements.Compatible x
t : P.obj X.op
ht : FamilyOfElements.IsAmalgamation x t
⊢ t = x (𝟙 X) (_ : singleton (𝟙 X) (𝟙 X))
simpa using ht _ (Presieve.singleton_self _)