English
For families of multiplicative equivalences es and fs indexed by η, the pi-congruence right-transpose distributes over trans.
Русский
Для семей эквивалентностей es и fs индексируемых по η, правое конгруэнтное преобразование распространяется через композицию.
LaTeX
$$$\bigl(\mathrm{piCongrRight}\, es\bigr).\mathrm{trans}\bigl(\mathrm{piCongrRight}\, fs\bigr) = \mathrm{piCongrRight}\, (\lambda i. (es\,i).trans (fs\,i)).$$$
Lean4
@[to_additive (attr := simp)]
theorem piCongrRight_trans {η : Type*} {Ms Ns Ps : η → Type*} [∀ j, Mul (Ms j)] [∀ j, Mul (Ns j)] [∀ j, Mul (Ps j)]
(es : ∀ j, Ms j ≃* Ns j) (fs : ∀ j, Ns j ≃* Ps j) :
(piCongrRight es).trans (piCongrRight fs) = piCongrRight fun i => (es i).trans (fs i) :=
rfl
