case a
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
⊢ ∀ (j : WalkingMulticospan I.fstTo I.sndTo),
    (forget C).map (limit.π (MulticospanIndex.multicospan I) j) x =
      (forget C).map (limit.π (MulticospanIndex.multicospan I) j) y
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
⊢ x = y
apply Concrete.limit_ext
case a.left
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
a : I.L
⊢ (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) x =
    (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) y

case a.right
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
b : I.R
⊢ (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) x =
    (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) y
case a
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
⊢ ∀ (j : WalkingMulticospan I.fstTo I.sndTo),
    (forget C).map (limit.π (MulticospanIndex.multicospan I) j) x =
      (forget C).map (limit.π (MulticospanIndex.multicospan I) j) y
rintro (a | b)
no goals
case a.left
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
a : I.L
⊢ (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) x =
    (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) y
apply h
no goals
case a.right
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), (forget C).map (Multiequalizer.ι I t) x = (forget C).map (Multiequalizer.ι I t) y
b : I.R
⊢ (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) x =
    (forget C).map (limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) y
rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), comp_apply, comp_apply, h]