Theorem: Int.add_twice_eq_mul_two (UnitConjecture/TorsionFree.lean)

State before:
a : ℤ
⊢ a + a = a * 2
Tactic:
rw [show (2 : ℤ) = 1 + 1 by rfl, mul_add, mul_one]
State after:
no goals

State before:
a : ℤ
⊢ 2 = 1 + 1
Tactic:
rfl
State after:
no goals