English
In the opposite setting, the equation with op and eqToHom preserves the same compatibility: (homOfLE h).op ≫ eqToHom hbc = homOfLE(hbc.trans (le_of_eq (op_injective hbc.symm))).op.
Русский
В противоположной обстановке равенство с операцией и eqToHom сохраняет ту же совместимость: (homOfLE h).op ∘ eqToHom hbc = homOfLE(...).op.
LaTeX
$$$\mathrm{homOfLE\_op\_comp\_eqToHom} : {a b c : X} (hab : b \le a) (hbc : op b = op c) \\Rightarrow (\mathrm{homOfLE}\,hab).op \circ \mathrm{eqToHom}(hbc) = \mathrm{homOfLE}(\, (hbc.trans (\mathrm{le\_of\_eq}(\mathrm{op\_injective}\, hbc.symm))) ).\mathrm{op}$$$
Lean4
@[simp, reassoc]
theorem homOfLE_op_comp_eqToHom {a b c : X} (hab : b ≤ a) (hbc : op b = op c) :
(homOfLE hab).op ≫ eqToHom hbc = (homOfLE ((le_of_eq (op_injective hbc.symm)).trans hab)).op :=
rfl
