Theorem: LoVe.Rat.div_two_add_div_two (LoVe/LoVelib.lean)

State before:
x : ℚ
⊢ x / 2 + x / 2 = x
Tactic:
have hxx : x + x = 2 * x :=
  by linarith
State after:
x : ℚ
hxx : x + x = 2 * x
⊢ x / 2 + x / 2 = x

State before:
x : ℚ
hxx : x + x = 2 * x
⊢ x / 2 + x / 2 = x
Tactic:
have hxx2 : (x + x) / 2 = (2 * x) / 2 :=
  by rw [hxx]
State after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x

State before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Tactic:
have hx2x2 : x / 2 + x / 2 = (2 * x) / 2 :=
  by
    rw [←hxx2]
    rw [add_div]
State after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x

State before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = x
Tactic:
rw [hx2x2]
State after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ 2 * x / 2 = x

State before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
hx2x2 : x / 2 + x / 2 = 2 * x / 2
⊢ 2 * x / 2 = x
Tactic:
ring
State after:
no goals

State before:
x : ℚ
⊢ x + x = 2 * x
Tactic:
linarith
State after:
no goals

State before:
x : ℚ
hxx : x + x = 2 * x
⊢ (x + x) / 2 = 2 * x / 2
Tactic:
rw [hxx]
State after:
no goals

State before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = 2 * x / 2
Tactic:
rw [←hxx2]
State after:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = (x + x) / 2

State before:
x : ℚ
hxx : x + x = 2 * x
hxx2 : (x + x) / 2 = 2 * x / 2
⊢ x / 2 + x / 2 = (x + x) / 2
Tactic:
rw [add_div]
State after:
no goals