Theorem: sum_eq_three_even (ListPowersProblem.lean)

State before:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j ^ 2 + j) + 1
Tactic:
simp [pow_two]
State after:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1

State before:
j : ℕ
⊢ sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
Tactic:
induction' j with j ih
State after:
case zero

⊢ sum (fun i => i + i / 2 + 1) (Nat.zero + Nat.zero) = 3 * (Nat.zero * Nat.zero + Nat.zero) + 1

case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1

State before:
case zero

⊢ sum (fun i => i + i / 2 + 1) (Nat.zero + Nat.zero) = 3 * (Nat.zero * Nat.zero + Nat.zero) + 1
Tactic:
rfl
State after:
no goals

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1
Tactic:
have hlt : 0 < 2 := by decide
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1
Tactic:
simp only [
  Nat.add_succ, add_zero, Nat.succ_add, sum_succ, ih, Nat.mul_succ, Nat.succ.injEq
]
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))
Tactic:
have h1 : Nat.succ j = j + 1 := rfl
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))
Tactic:
have h2 : Nat.succ (j + j) = j + j + 1 := rfl
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))
Tactic:
have h3 : Nat.succ (j + j + 1) = j + j + 2 := rfl
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))
Tactic:
rw [h1, h2, h3]
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ 3 * (j * j + j) + (j + j + (j + j + 1) / 2) + (j + j + (j + j + 2) / 2) = Nat.succ (3 * ((j + 1) * j + j + j))

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ 3 * (j * j + j) + (j + j + (j + j + 1) / 2) + (j + j + (j + j + 2) / 2) = Nat.succ (3 * ((j + 1) * j + j + j))
Tactic:
ring_nf
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + (1 + j * 2) / 2 + (2 + j * 2) / 2 = Nat.succ (j * 9 + j ^ 2 * 3)

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + (1 + j * 2) / 2 + (2 + j * 2) / 2 = Nat.succ (j * 9 + j ^ 2 * 3)
Tactic:
rw [Nat.add_div hlt, Nat.mul_div hlt]
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + (1 / 2 + j + if 2 ≤ 1 % 2 + j * 2 % 2 then 1 else 0) + (2 + j * 2) / 2 =
    Nat.succ (j * 9 + j ^ 2 * 3)

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + (1 / 2 + j + if 2 ≤ 1 % 2 + j * 2 % 2 then 1 else 0) + (2 + j * 2) / 2 =
    Nat.succ (j * 9 + j ^ 2 * 3)
Tactic:
simp [
  show 1 / 2 = 0 from rfl,
  show ∀ x, Nat.succ x = x + 1 from fun _ => rfl
]
State after:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + j + (j + 1) = j * 9 + j ^ 2 * 3 + 1

State before:
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
h1 : Nat.succ j = j + 1
h2 : Nat.succ (j + j) = j + j + 1
h3 : Nat.succ (j + j + 1) = j + j + 2
⊢ j * 7 + j ^ 2 * 3 + j + (j + 1) = j * 9 + j ^ 2 * 3 + 1
Tactic:
ring
State after:
no goals

State before:
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
⊢ 0 < 2
Tactic:
decide
State after:
no goals