case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ ∃ S y, x = mk y
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
⊢ ∃ S y, x = mk y
obtain ⟨S, y, h⟩ := Concrete.colimit_exists_rep (J.diagram P X) x
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ x = mk (↑(Meq.equiv P S.unop) y)
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ ∃ S y, x = mk y
use S.unop, Meq.equiv _ _ y
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ (forget D).map (colimit.ι (diagram J P X) S) y = mk (↑(Meq.equiv P S.unop) y)
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ x = mk (↑(Meq.equiv P S.unop) y)
rw [← h]
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ (forget D).map (colimit.ι (diagram J P X) S) y =
    (forget D).map (colimit.ι (diagram J P X) S) (↑(Meq.equiv P S.unop).symm (↑(Meq.equiv P S.unop) y))
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ (forget D).map (colimit.ι (diagram J P X) S) y = mk (↑(Meq.equiv P S.unop) y)
dsimp [mk]
no goals
case intro.intro
C : Type u
inst✝⁶ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category D
inst✝⁴ : ConcreteCategory D
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
x : (forget D).obj ((plusObj J P).obj X.op)
S : (Cover J X)ᵒᵖ
y : (forget D).obj ((diagram J P X).obj S)
h : (forget D).map (colimit.ι (diagram J P X) S) y = x
⊢ (forget D).map (colimit.ι (diagram J P X) S) y =
    (forget D).map (colimit.ι (diagram J P X) S) (↑(Meq.equiv P S.unop).symm (↑(Meq.equiv P S.unop) y))
simp