Theorem: Poland1998P4.lemma7 (Compfiles/Poland1998P4.lean)

State before:
n : ℕ
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
have h1 : (4 * (n - 1) + 1 + 5) = 2 * (2 * (n - 1) + 1 + 2) := by ring
State after:
n : ℕ
h1 : 4 * (n - 1) + 1 + 5 = 2 * (2 * (n - 1) + 1 + 2)
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2

State before:
n : ℕ
h1 : (4 * (n - 1) + 1 + 5) / 2 = 2 * (2 * (n - 1) + 1 + 2) / 2
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
rwa[Nat.mul_div_right _ (show 0 < 2 by norm_num)] at h1
State after:
no goals

State before:
n : ℕ
⊢ 4 * (n - 1) + 1 + 5 = 2 * (2 * (n - 1) + 1 + 2)
Tactic:
ring
State after:
no goals

State before:
n : ℕ
h1 : (4 * (n - 1) + 1 + 5) / 2 = 2 * (2 * (n - 1) + 1 + 2) / 2
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals