C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = γ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ η = γ
have : γ = J.plusLift (J.toPlus P ≫ γ) hQ := by
  apply plusLift_unique
  rfl
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = plusLift J (toPlus J P ≫ γ) hQ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = γ
rw [this]
case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ toPlus J P ≫ η = toPlus J P ≫ γ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ η = plusLift J (toPlus J P ≫ γ) hQ
apply plusLift_unique
no goals
case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
this : γ = plusLift J (toPlus J P ≫ γ) hQ
⊢ toPlus J P ≫ η = toPlus J P ≫ γ
exact h
case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ toPlus J P ≫ γ = toPlus J P ≫ γ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ γ = plusLift J (toPlus J P ≫ γ) hQ
apply plusLift_unique
no goals
case hγ
C : Type u
inst✝³ : Category C
J : GrothendieckTopology C
D : Type w
inst✝² : Category D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
P✝ : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : plusObj J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toPlus J P ≫ η = toPlus J P ≫ γ
⊢ toPlus J P ≫ γ = toPlus J P ≫ γ
rfl