Tactic.Elementwise.hom_elementwise

theorem Tactic.Elementwise.hom_elementwise : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C} {f g : X ⟶ Y}, f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x

This theorem, `Tactic.Elementwise.hom_elementwise`, states that for any concrete category `C`, given two morphisms `f` and `g` from object `X` to object `Y` in `C`, if `f` and `g` are equal, then the action of `f` and `g` on any element `x` of the type associated to `X` by the forgetful functor from `C` to `Type` are also equal. In simpler terms, if two morphisms are equal, then their action on any element of the object they originate from is also equal.

More concisely: If morphisms `f` and `g` in category `C` from object `X` to object `Y` are equal, then for all `x : X`, `f x = g x`.