case mp
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
S T : Cover J X
x : Meq P S
y : Meq P T
⊢ mk x = mk y → ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2

case mpr
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
S T : Cover J X
x : Meq P S
y : Meq P T
⊢ (∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2) → mk 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
S T : Cover J X
x : Meq P S
y : Meq P T
⊢ mk x = mk y ↔ ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
constructor
case mp
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
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
⊢ ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
case mp
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
S T : Cover J X
x : Meq P S
y : Meq P T
⊢ mk x = mk y → ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
intro h
case mp.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
⊢ ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
case mp
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
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
⊢ ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq _ _ _ h
case mp.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
⊢ Meq.refine x h1.unop = Meq.refine y h2.unop
case mp.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
⊢ ∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2
use W.unop, h1.unop, h2.unop
case mp.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
I : Cover.Arrow W.unop
⊢ ↑(Meq.refine x h1.unop) I = ↑(Meq.refine y h2.unop) I
case mp.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
⊢ Meq.refine x h1.unop = Meq.refine y h2.unop
ext I
case mp.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
⊢ ↑(Meq.refine x h1.unop) I = ↑(Meq.refine y h2.unop) I
case mp.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
hh :
  (forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x) =
    (forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y)
I : Cover.Arrow W.unop
⊢ ↑(Meq.refine x h1.unop) I = ↑(Meq.refine y h2.unop) I
apply_fun Multiequalizer.ι (W.unop.index P) I  at hh
case h.e'_2.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑(Meq.refine x h1.unop) I =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x))

case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑(Meq.refine y h2.unop) I =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
case mp.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
⊢ ↑(Meq.refine x h1.unop) I = ↑(Meq.refine y h2.unop) I
convert hh
no goals
case h.e'_2.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑(Meq.refine x h1.unop) I =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x))

case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑(Meq.refine y h2.unop) I =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
all_goals
  dsimp [diagram]
  simp only [← comp_apply, Multiequalizer.lift_ι, Category.comp_id, Meq.equiv_symm_eq_apply]
  cases I; rfl
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑y { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) T).arrows I.f) } =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map
        (Multiequalizer.lift (Cover.index W.unop P) (multiequalizer (Cover.index T P))
          (fun I => Multiequalizer.ι (Cover.index T P) (Cover.Arrow.map I h2.unop))
          (_ :
            ∀ (I : (Cover.index W.unop P).R),
              Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.fstTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)) ≫
                  MulticospanIndex.fst (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop) =
                Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.sndTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)) ≫
                  MulticospanIndex.snd (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)))
        (↑(Meq.equiv P T).symm y))
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑(Meq.refine y h2.unop) I =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
dsimp [diagram]
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑y { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) T).arrows I.f) } = ↑y (Cover.Arrow.map I h2.unop)
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑y { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) T).arrows I.f) } =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map
        (Multiequalizer.lift (Cover.index W.unop P) (multiequalizer (Cover.index T P))
          (fun I => Multiequalizer.ι (Cover.index T P) (Cover.Arrow.map I h2.unop))
          (_ :
            ∀ (I : (Cover.index W.unop P).R),
              Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.fstTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)) ≫
                  MulticospanIndex.fst (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop) =
                Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.sndTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)) ≫
                  MulticospanIndex.snd (Cover.index T.op.unop P) (Cover.Relation.map I h2.unop)))
        (↑(Meq.equiv P T).symm y))
simp only [← comp_apply, Multiequalizer.lift_ι, Category.comp_id, Meq.equiv_symm_eq_apply]
case h.e'_3.h.mk
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
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (Cover.sieve W.unop).arrows f✝
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ :
  (forget D).obj (P.obj { Y := Y✝, f := f✝, hf := hf✝ }.Y.op) =
    (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑y
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f,
        hf := (_ : ((fun a => ↑a) T).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f) } =
    ↑y (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } h2.unop)
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
I : Cover.Arrow W.unop
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) I)
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ : (forget D).obj (P.obj I.Y.op) = (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) I)
⊢ ↑y { Y := I.Y, f := I.f, hf := (_ : ((fun a => ↑a) T).arrows I.f) } = ↑y (Cover.Arrow.map I h2.unop)
cases I
no goals
case h.e'_3.h.mk
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
S T : Cover J X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (Cover J X)ᵒᵖ
h1 : S.op ⟶ W
h2 : T.op ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (Cover.sieve W.unop).arrows f✝
hh :
  (forget D).map (Multiequalizer.ι (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
      ((forget D).map ((diagram J P X).map h1) (↑(Meq.equiv P S).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
      ((forget D).map ((diagram J P X).map h2) (↑(Meq.equiv P T).symm y))
e_1✝ :
  (forget D).obj (P.obj { Y := Y✝, f := f✝, hf := hf✝ }.Y.op) =
    (forget D).obj (MulticospanIndex.left (Cover.index W.unop P) { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑y
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f,
        hf := (_ : ((fun a => ↑a) T).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f) } =
    ↑y (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } h2.unop)
rfl
case mpr.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ mk x = mk y
case mpr
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
S T : Cover J X
x : Meq P S
y : Meq P T
⊢ (∃ W h1 h2, Meq.refine x h1 = Meq.refine y h2) → mk x = mk y
rintro ⟨S, h1, h2, e⟩
case mpr.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ ∃ k f g,
    (forget D).map ((diagram J P X).map f) (↑(Meq.equiv P S✝).symm x) =
      (forget D).map ((diagram J P X).map g) (↑(Meq.equiv P T).symm y)
case mpr.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ mk x = mk y
apply Concrete.colimit_rep_eq_of_exists
case mpr.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ (forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x) =
    (forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y)
case mpr.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ ∃ k f g,
    (forget D).map ((diagram J P X).map f) (↑(Meq.equiv P S✝).symm x) =
      (forget D).map ((diagram J P X).map g) (↑(Meq.equiv P T).symm y)
use op S, h1.op, h2.op
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ ∀ (t : (Cover.index S.op.unop P).L),
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) t)
        ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
      (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) t)
        ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
case mpr.intro.intro.intro.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ (forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x) =
    (forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y)
apply Concrete.multiequalizer_ext
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
i : (Cover.index S.op.unop P).L
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
⊢ ∀ (t : (Cover.index S.op.unop P).L),
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) t)
        ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
      (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) t)
        ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
intro i
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
e : Meq.refine x h1 = Meq.refine y h2
i : (Cover.index S.op.unop P).L
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
apply_fun fun ee => ee i  at e
case h.e'_2.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    ↑(Meq.refine x h1) i

case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y)) =
    ↑(Meq.refine y h2) i
case mpr.intro.intro.intro.h.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y))
convert e
no goals
case h.e'_2.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h1.op) (↑(Meq.equiv P S✝).symm x)) =
    ↑(Meq.refine x h1) i

case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y)) =
    ↑(Meq.refine y h2) i
all_goals
  dsimp [diagram]
  simp only [← comp_apply, Multiequalizer.lift_ι, Meq.equiv_symm_eq_apply]
  cases i; rfl
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S P) i)
      ((forget D).map
        (Multiequalizer.lift (Cover.index S P) (multiequalizer (Cover.index T P))
          (fun I => Multiequalizer.ι (Cover.index T P) (Cover.Arrow.map I h2))
          (_ :
            ∀ (I : (Cover.index S.op.unop P).R),
              Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.fstTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)) ≫
                  MulticospanIndex.fst (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop) =
                Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.sndTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)) ≫
                  MulticospanIndex.snd (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)))
        (↑(Meq.equiv P T).symm y)) =
    ↑y { Y := i.Y, f := i.f, hf := (_ : ((fun a => ↑a) T).arrows i.f) }
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S.op.unop P) i)
      ((forget D).map ((diagram J P X).map h2.op) (↑(Meq.equiv P T).symm y)) =
    ↑(Meq.refine y h2) i
dsimp [diagram]
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := (_ : ((fun a => ↑a) T).arrows i.f) }
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ (forget D).map (Multiequalizer.ι (Cover.index S P) i)
      ((forget D).map
        (Multiequalizer.lift (Cover.index S P) (multiequalizer (Cover.index T P))
          (fun I => Multiequalizer.ι (Cover.index T P) (Cover.Arrow.map I h2))
          (_ :
            ∀ (I : (Cover.index S.op.unop P).R),
              Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.fstTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)) ≫
                  MulticospanIndex.fst (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop) =
                Multiequalizer.ι (Cover.index T.op.unop P)
                    (MulticospanIndex.sndTo (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)) ≫
                  MulticospanIndex.snd (Cover.index T.op.unop P) (Cover.Relation.map I h2.op.unop)))
        (↑(Meq.equiv P T).symm y)) =
    ↑y { Y := i.Y, f := i.f, hf := (_ : ((fun a => ↑a) T).arrows i.f) }
simp only [← comp_apply, Multiequalizer.lift_ι, Meq.equiv_symm_eq_apply]
case h.e'_3.h.mk
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
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (Cover.sieve S.op.unop).arrows f✝
e : ↑(Meq.refine x h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(Meq.refine y h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) { Y := Y✝, f := f✝, hf := hf✝ }) =
    (forget D).obj (P.obj { Y := Y✝, f := f✝, hf := hf✝ }.Y.op)
⊢ ↑y (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } h2) =
    ↑y
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f,
        hf := (_ : ((fun a => ↑a) T).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f) }
case h.e'_3.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)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (Cover.index S.op.unop P).L
e : ↑(Meq.refine x h1) i = ↑(Meq.refine y h2) i
e_1✝ : (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) i) = (forget D).obj (P.obj i.Y.op)
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := (_ : ((fun a => ↑a) T).arrows i.f) }
cases i
no goals
case h.e'_3.h.mk
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
S✝ T : Cover J X
x : Meq P S✝
y : Meq P T
S : Cover J X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (Cover.sieve S.op.unop).arrows f✝
e : ↑(Meq.refine x h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(Meq.refine y h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  (forget D).obj (MulticospanIndex.left (Cover.index S.op.unop P) { Y := Y✝, f := f✝, hf := hf✝ }) =
    (forget D).obj (P.obj { Y := Y✝, f := f✝, hf := hf✝ }.Y.op)
⊢ ↑y (Cover.Arrow.map { Y := Y✝, f := f✝, hf := hf✝ } h2) =
    ↑y
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f,
        hf := (_ : ((fun a => ↑a) T).arrows { Y := Y✝, f := f✝, hf := hf✝ }.f) }
rfl