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

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

State before:
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ (4 * (n - 1) + 1 + 3) / 2 = 2 * (n - 1) + 1 + 1
Tactic:
rw [this, Nat.mul_div_right]
State after:
case H
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ 0 < 2

State before:
case H
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ 0 < 2
Tactic:
exact two_pos
State after:
no goals

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