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 ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) (_ : True)
⊢ t₁ = 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
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
⊢ t₁ = t₂
have q₁ := h₁ (𝟙 X) (by tauto)
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 ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) (_ : True)
q₂ : P.map (𝟙 X).op t₂ = x (𝟙 X) (_ : True)
⊢ t₁ = 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
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) (_ : True)
⊢ t₁ = t₂
have q₂ := h₂ (𝟙 X) (by tauto)
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 ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : t₁ = x (𝟙 X) (_ : True)
q₂ : t₂ = x (𝟙 X) (_ : True)
⊢ t₁ = 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
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) (_ : True)
q₂ : P.map (𝟙 X).op t₂ = x (𝟙 X) (_ : True)
⊢ t₁ = t₂
simp only [op_id, FunctorToTypes.map_id_apply] at q₁ q₂
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : t₁ = x (𝟙 X) (_ : True)
q₂ : t₂ = x (𝟙 X) (_ : True)
⊢ t₁ = t₂
rw [q₁, q₂]
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
⊢ ⊤ (𝟙 X)
tauto
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
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj X.op
h₁ : FamilyOfElements.IsAmalgamation x t₁
h₂ : FamilyOfElements.IsAmalgamation x t₂
q₁ : P.map (𝟙 X).op t₁ = x (𝟙 X) (_ : True)
⊢ ⊤ (𝟙 X)
tauto