-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
h :
  ∀ (x : A),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inl x) =
      TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
              (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                  Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T)
                    x
                    (fun (x : A) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                          (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                        x)
                    fun (x : B) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                        (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                      x :
                Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
            f₁ f₂))
        (Sum.inl x)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      x
have h₃ : ∀ (x : B),
  (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inr x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inr x)
Tactic: rcases x with x | x
Cleared hypotheses: x