English
Simp lemmas simplify addition on the localized module via mk and alignment with equations.
Русский
Леммы simp упрощают сложение в локализованном модуле через mk и выравнивание по уравнениям.
LaTeX
$$$\\text{simp} : mk(a) + mk(b) = mk(a_{1}+b_{1}, a_{2}b_{2})$$$
Lean4
instance : Add (LocalizedModule S M) where
add p1
p2 :=
liftOn₂ p1 p2 (fun x y => mk (y.2 • x.1 + x.2 • y.1) (x.2 * y.2)) <|
fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨m1', s1'⟩ ⟨m2', s2'⟩ ⟨u1, hu1⟩ ⟨u2, hu2⟩ =>
mk_eq.mpr
⟨u1 * u2, by
-- Put everything in the same shape, sorting the terms using `simp`
have hu1' := congr_arg ((u2 * s2 * s2') • ·) hu1
have hu2' := congr_arg ((u1 * s1 * s1') • ·) hu2
simp only [smul_add, ← mul_smul, mul_comm, mul_left_comm] at hu1' hu2' ⊢
rw [hu1', hu2']⟩
