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)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ ∀ (j : WidePullbackShape ι),
    (forget C).map (limit.π (wideCospan B X f) j) x = (forget C).map (limit.π (wideCospan B X f) 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)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ x = y
apply Concrete.limit_ext
case a.none
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ (forget C).map (limit.π (wideCospan B X f) none) x = (forget C).map (limit.π (wideCospan B X f) none) y

case a.some
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
j : ι
⊢ (forget C).map (limit.π (wideCospan B X f) (some j)) x = (forget C).map (limit.π (wideCospan B X f) (some j)) 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)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ ∀ (j : WidePullbackShape ι),
    (forget C).map (limit.π (wideCospan B X f) j) x = (forget C).map (limit.π (wideCospan B X f) j) y
rintro (_ | j)
no goals
case a.none
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
⊢ (forget C).map (limit.π (wideCospan B X f) none) x = (forget C).map (limit.π (wideCospan B X f) none) y
exact h₀
no goals
case a.some
C : Type u
inst✝⁵ : Category C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : (forget C).map (base f) x = (forget C).map (base f) y
h : ∀ (j : ι), (forget C).map (π f j) x = (forget C).map (π f j) y
j : ι
⊢ (forget C).map (limit.π (wideCospan B X f) (some j)) x = (forget C).map (limit.π (wideCospan B X f) (some j)) y
apply h