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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : (forget D).map ((toPlus J P).app X.op) x = (forget D).map ((toPlus J P).app X.op) y
⊢ x = 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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
⊢ Function.Injective ((forget D).map ((toPlus J P).app X.op))
intro x y h
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ x = 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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : (forget D).map ((toPlus J P).app X.op) x = (forget D).map ((toPlus J P).app X.op) y
⊢ x = y
simp only [toPlus_eq_mk] at h
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : ∃ W h1 h2, Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ x = 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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ x = y
rw [eq_mk_iff_exists] at h
case intro.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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ x = 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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
h : ∃ W h1 h2, Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ x = y
obtain ⟨W, h1, h2, hh⟩ := h
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ ∀ (I : Cover.Arrow W), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
case intro.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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ x = y
apply hsep X W
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
I : Cover.Arrow W
⊢ (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
⊢ ∀ (I : Cover.Arrow W), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
intro I
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
I : Cover.Arrow W
hh : ↑(Meq.refine (Meq.mk ⊤ x) h1) I = ↑(Meq.refine (Meq.mk ⊤ y) h2) I
⊢ (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
hh : Meq.refine (Meq.mk ⊤ x) h1 = Meq.refine (Meq.mk ⊤ y) h2
I : Cover.Arrow W
⊢ (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
apply_fun fun e => e I  at hh
no goals
case intro.intro.intro.a
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
x y : (forget D).obj (P.obj X.op)
W : Cover J X
h1 h2 : W ⟶ ⊤
I : Cover.Arrow W
hh : ↑(Meq.refine (Meq.mk ⊤ x) h1) I = ↑(Meq.refine (Meq.mk ⊤ y) h2) I
⊢ (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y
exact hh