Theorem: ℤα.coe_sub (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a - b) = OneHom.toFun (↑↑inclusion) a - OneHom.toFun (↑↑inclusion) b
Tactic:
change ((a + -b : ℤα) : ℂ) = a + -(b : ℂ)
State after:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + -OneHom.toFun (↑↑inclusion) b

State before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + -OneHom.toFun (↑↑inclusion) b
Tactic:
rw [← coe_neg]
State after:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + OneHom.toFun (↑↑inclusion) (-b)

State before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + OneHom.toFun (↑↑inclusion) (-b)
Tactic:
exact my_map_add a (-b)
State after:
no goals