English
If e is an equivalence and eq relates ra and rb, then the induced Quotient congr maps mk ra a to mk rb (e a).
Русский
Если e — эквивалентность и eq связывает ra и rb, то полученная конгруэнция на квотах отправляет mk ra a в mk rb (e a).
LaTeX
$$$ \forall (e:Equiv α β) (eq:∀ a_1 a_2, ra a_1 a_2 \leftrightarrow rb (e a_1) (e a_2)) (a:α),\ EquivLike.toFunLike.coe (Quotient.congr e eq) (Quotient.mk ra a) = Quotient.mk rb (e a) $$$
Lean4
@[simp]
theorem congr_mk {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ a₁ a₂ : α, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :
Quotient.congr e eq (Quotient.mk ra a) = Quotient.mk rb (e a) :=
rfl
