Theorem: add_self_eq_mul_two (ECTate/Algebra/Ring/Basic.lean)

State before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ a + a = 2 * a
Tactic:
rw [←one_mul a, ←add_mul, one_mul]
State after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (1 + 1) * a = 2 * a

State before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (1 + 1) * a = 2 * a
Tactic:
congr
State after:
case e_a
R : Type u_1
inst✝ : Semiring R
a : R
⊢ 1 + 1 = 2

State before:
case e_a
R : Type u_1
inst✝ : Semiring R
a : R
⊢ 1 + 1 = 2
Tactic:
norm_num
State after:
no goals