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

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

State before:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (4 * (n - 1) + 1 + 6) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
rw [h1]
State after:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (2 * (2 * (n - 1) + 1 + 2) + 1) / 2 = 2 * (n - 1) + 1 + 2

State before:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (2 * (2 * (n - 1) + 1 + 2) + 1) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
exact lemma2 (2 * (n - 1) + 1 + 2)
State after:
no goals

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