English
For a fixed y ∈ M, let u_y be the unit in P corresponding to g(y). Then for all w,z1,z2 ∈ P, w · u_y^{-1} + z1 = z2 if and only if w + u_y z1 = u_y z2.
Русский
Для фиксированного y ∈ M пусть u_y — единица в P, соответствующая g(y). Тогда для любых w, z1, z2 ∈ P выполняется равенство w · u_y^{-1} + z1 = z2 тогда и только тогда, когда w + u_y z1 = u_y z2.
LaTeX
$$$ w \\cdot u_y^{-1} + z_1 = z_2 \\iff w + u_y \\cdot z_1 = u_y \\cdot z_2, \\quad y \\in M, \\ w,z_1,z_2 \\in P, \\ u_y = \\mathrm{IsUnit.liftRight}(\\cdot) . $$$
Lean4
theorem mul_add_inv_left {g : R →+* P} (h : ∀ y : M, IsUnit (g y)) (y : M) (w z₁ z₂ : P) :
w * ↑(IsUnit.liftRight (g.toMonoidHom.restrict M) h y)⁻¹ + z₁ = z₂ ↔ w + g y * z₁ = g y * z₂ :=
by
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y), mul_assoc, ← mul_add,
Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left, IsUnit.coe_liftRight]
simp [RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply]
