English
If c relates x to y, and a derived condition on f holds (hf), then c(fx) relates to c(fy).
Русский
Если c связывает x и y и выполняется условие hf, то c(fx) связывает c(fy).
LaTeX
$$$\\forall x,y\\, (c\\,x\\,y) \\Rightarrow (c\\,f\\,x\\,f\\,y)$ under hf condition$$
Lean4
/-- Sometimes, a group is defined as a quotient of a monoid by a congruence relation.
Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
and `∀ x, c (f x * x) 1` (to prove the group laws), one can only prove the latter. -/
@[to_additive /-- Sometimes, an additive group is defined as a quotient of a monoid
by an additive congruence relation.
Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
and `∀ x, c (f x + x) 0` (to prove the group laws), one can only prove the latter. -/
]
theorem map_of_mul_left_rel_one [Monoid M] (c : Con M) (f : M → M) (hf : ∀ x, c (f x * x) 1) {x y} (h : c x y) :
c (f x) (f y) := by
simp only [← Con.eq, coe_one, coe_mul] at *
have hf' : ∀ x : M, (x : c.Quotient) * f x = 1 := fun x ↦
calc
(x : c.Quotient) * f x = f (f x) * f x * (x * f x) := by simp [hf]
_ = f (f x) * (f x * x) * f x := by simp_rw [mul_assoc]
_ = 1 := by simp [hf]
have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h
exact congr_arg Units.inv this
