-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
theorem multiequalizer_ext {J : MulticospanShape.{w, w'}}
    {I : MulticospanIndex J C} [HasMultiequalizer I]
    [PreservesLimit I.multicospan (forget C)] (x y : ToType (multiequalizer I))
    (h : ∀ t : J.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) 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 w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
⊢ ∀ (j : WalkingMulticospan J),
    (ConcreteCategory.hom (limit.π I.multicospan j)) x = (ConcreteCategory.hom (limit.π I.multicospan j)) y

Proof state:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
⊢ ∀ (j : WalkingMulticospan J),
    (ConcreteCategory.hom (limit.π I.multicospan j)) x = (ConcreteCategory.hom (limit.π I.multicospan j)) y

Tactic:
rintro (a | b)

Result:
case a.left
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
a : J.L
⊢ (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left a))) x =
    (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left a))) y

case a.right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.right b))) x =
    (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.right b))) y

Proof state:
case a.left
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
a : J.L
⊢ (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left a))) x =
    (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left a))) y

Tactic:
apply h

Result:
no goals

Proof state:
case a.right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) x) =
    (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) y)

Tactic:
simp [h]

Result:
no goals

Proof state:
case a.right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.right b))) x =
    (ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.right b))) y

Tactic:
rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ConcreteCategory.comp_apply,
  ConcreteCategory.comp_apply]

Result:
case a.right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w w' v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) x) =
    (ConcreteCategory.hom (I.multicospan.map (WalkingMulticospan.Hom.fst b)))
      ((ConcreteCategory.hom (limit.π I.multicospan (WalkingMulticospan.left (J.fst b)))) y)