-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem widePullback_ext {B : C} {ι : Type w} {X : ι → C} (f : ∀ j : ι, X j ⟶ B)
    [HasWidePullback B X f] [PreservesLimit (wideCospan B X f) (forget C)]
    (x y : ToType (widePullback B X f)) (h₀ : base f x = base f y) (h : ∀ j, π f j x = π f j y) :
    x = y

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ x = y

Tactic:
apply Concrete.limit_ext

Result:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ ∀ (j : WidePullbackShape ι),
    (ConcreteCategory.hom (limit.π (wideCospan B X f) j)) x = (ConcreteCategory.hom (limit.π (wideCospan B X f) j)) y

Proof state:
case a.none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ (ConcreteCategory.hom (limit.π (wideCospan B X f) none)) x =
    (ConcreteCategory.hom (limit.π (wideCospan B X f) none)) y

Tactic:
exact h₀

Result:
no goals

Proof state:
case a.some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
j : ι
⊢ (ConcreteCategory.hom (limit.π (wideCospan B X f) (some j))) x =
    (ConcreteCategory.hom (limit.π (wideCospan B X f) (some j))) y

Tactic:
apply h

Result:
no goals

Proof state:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ ∀ (j : WidePullbackShape ι),
    (ConcreteCategory.hom (limit.π (wideCospan B X f) j)) x = (ConcreteCategory.hom (limit.π (wideCospan B X f) j)) y

Tactic:
rintro (_ | j)

Result:
case a.none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
⊢ (ConcreteCategory.hom (limit.π (wideCospan B X f) none)) x =
    (ConcreteCategory.hom (limit.π (wideCospan B X f) none)) y

case a.some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
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 : ToType (widePullback B X f)
h₀ : (ConcreteCategory.hom (base f)) x = (ConcreteCategory.hom (base f)) y
h : ∀ (j : ι), (ConcreteCategory.hom (π f j)) x = (ConcreteCategory.hom (π f j)) y
j : ι
⊢ (ConcreteCategory.hom (limit.π (wideCospan B X f) (some j))) x =
    (ConcreteCategory.hom (limit.π (wideCospan B X f) (some j))) y