Theorem: sum_nats (ListPowersProblem.lean)

State before:
⊢ sum nats = fun i => i * (i + 1) / 2
Tactic:
simp [nats, pow_two]
State after:
⊢ (sum fun n => n) = fun i => i * (i + 1) / 2

State before:
⊢ (sum fun n => n) = fun i => i * (i + 1) / 2
Tactic:
funext i
State after:
case h
i : ℕ
⊢ sum (fun n => n) i = i * (i + 1) / 2

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

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

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

State before:
case h.zero

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

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ sum (fun n => n) (Nat.succ i) = Nat.succ i * (Nat.succ i + 1) / 2
Tactic:
simp only [sum_succ, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_div, 
  Nat.isUnit_iff]
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ Nat.succ ((i * i + i) / 2 + i) =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ Nat.succ ((i * i + i) / 2 + i) =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0
Tactic:
show _ + 1 = _
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0
Tactic:
have not_two_le : ¬2 ≤ (i * i + i) % 2 := by
  cases Nat.mod_two_eq_zero_or_one (i * i + i) <;> simp [*]
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ (i * i + i) / 2 + i + 1 =
    ((i * i + i + i + i) / 2 + if 2 ∣ Nat.succ (i * i + i + i + i) then 1 else 0) +
      if 2 ∣ Nat.succ (Nat.succ (i * i + i + i + i)) then 1 else 0
Tactic:
simp [
  Nat.add_assoc (i*i+i) i i, 
  Nat.add_div (a := i*i+i), 
  ←mul_two i,
  Nat.mul_div,
  not_two_le,
  Nat.add_assoc ((i * i + i) / 2 + i),
  Nat.dvd_iff_mod_eq_zero
]
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = 0 then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = 0 then 1 else 0
Tactic:
have : (Nat.succ (Nat.succ (i * i + i + i * 2))) % 2 
      = (Nat.succ ((Nat.succ (i * i + i + i * 2) % 2))) % 2 := by
  show (_ + 1) % 2 = _
  rw [Nat.add_mod]
  rfl
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
this : Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = 0 then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
this : Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = 0 then 1 else 0
Tactic:
rw [this]
State after:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
this : Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2 = 0 then 1 else 0

State before:
case h.succ
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
this : Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
⊢ 1 =
    (if Nat.succ (i * i + i + i * 2) % 2 = 0 then 1 else 0) +
      if Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2 = 0 then 1 else 0
Tactic:
cases' Nat.mod_two_eq_zero_or_one (Nat.succ (i * i + i + i * 2)) with h h
  <;> simp [h]
State after:
no goals

State before:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
⊢ ¬2 ≤ (i * i + i) % 2
Tactic:
cases Nat.mod_two_eq_zero_or_one (i * i + i) <;> simp [*]
State after:
no goals

State before:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ Nat.succ (Nat.succ (i * i + i + i * 2)) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
Tactic:
show (_ + 1) % 2 = _
State after:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ (i * i + i + i * 2 + 1 + 1) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2

State before:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ (i * i + i + i * 2 + 1 + 1) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
Tactic:
rw [Nat.add_mod]
State after:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ ((i * i + i + i * 2 + 1) % 2 + 1 % 2) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2

State before:
i : ℕ
ih : sum (fun n => n) i = i * (i + 1) / 2
not_two_le : ¬2 ≤ (i * i + i) % 2
⊢ ((i * i + i + i * 2 + 1) % 2 + 1 % 2) % 2 = Nat.succ (Nat.succ (i * i + i + i * 2) % 2) % 2
Tactic:
rfl
State after:
no goals