-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₁ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₁ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₂ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
have rw : Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) g₂ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
      { down := 0 } :
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) g₂ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
      { down := 0 } :
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
Tactic: rw [eq]