English
For an additive setting, if g x is an additive unit, then F.lift x hg (F a) = g a for all a.
Русский
В аддитивной обстановке, если g x является аддитивной единицей, то F.lift x hg (F a) = g a для каждого a.
LaTeX
$$$ F.lift x\ hg (F a) = g a $$$
Lean4
/-- The congruence relation used to localize a `CommMonoid` at a submonoid can be expressed
equivalently as an infimum (see `Localization.r`) or explicitly
(see `Localization.r'`). -/
@[to_additive /-- The additive congruence relation used to localize an `AddCommMonoid` at a submonoid can be
expressed equivalently as an infimum (see `AddLocalization.r`) or explicitly
(see `AddLocalization.r'`). -/
]
theorem r_eq_r' : r S = r' S :=
le_antisymm (sInf_le fun _ ↦ ⟨1, by simp⟩) <|
le_sInf fun b H ⟨p, q⟩ ⟨x, y⟩ ⟨t, ht⟩ ↦
by
rw [← one_mul (p, q), ← one_mul (x, y)]
refine b.trans (b.mul (H (t * y)) (b.refl _)) ?_
convert b.symm (b.mul (H (t * q)) (b.refl (x, y))) using 1
dsimp only [Prod.mk_mul_mk, Submonoid.coe_mul] at ht ⊢
simp_rw [mul_assoc, ht, mul_comm y q]
