internlm/Lean-Github huggingface dataset:
Theorem: sum_eq_three_even
Proof 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
Proof state after:
no goals
Theorem: sum_eq_three_even
Proof 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
Proof 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
Theorem: sum_eq_three_even
Proof 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
]
Proof 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))
Theorem: sum_eq_three_even
Proof 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
Proof 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))
Theorem: sum_eq_three_even
Proof 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
Proof 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))
Theorem: sum_eq_three_even
Proof 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
Proof 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))
Theorem: sum_eq_three_even
Proof 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]
Proof 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))
Theorem: sum_eq_three_even
Proof 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
Proof 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)
Theorem: sum_eq_three_even
Proof 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]
Proof 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)
Theorem: sum_eq_three_even
Proof 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
]
Proof 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
Theorem: sum_eq_three_even
Proof 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
Proof state after:
no goals
Theorem: sum_eq_three_even
Proof state before:
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: sum_nats
Proof state before:
⊢ sum nats = fun i => i * (i + 1) / 2
Tactic:
simp [nats, pow_two]
Proof state after:
⊢ (sum fun n => n) = fun i => i * (i + 1) / 2
Theorem: sum_nats
Proof state before:
⊢ (sum fun n => n) = fun i => i * (i + 1) / 2
Tactic:
funext i
Proof state after:
case h
i : ℕ
⊢ sum (fun n => n) i = i * (i + 1) / 2
Theorem: sum_nats
Proof state before:
case h
i : ℕ
⊢ sum (fun n => n) i = i * (i + 1) / 2
Tactic:
induction' i with i ih
Proof 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
Theorem: sum_nats
Proof state before:
case h.zero

⊢ sum (fun n => n) Nat.zero = Nat.zero * (Nat.zero + 1) / 2
Tactic:
rfl
Proof state after:
no goals
Theorem: sum_nats
Proof 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]
Proof 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
Theorem: sum_nats
Proof 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 = _
Proof 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
Theorem: sum_nats
Proof 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 [*]
Proof 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
Theorem: sum_nats
Proof 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
]
Proof 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
Theorem: sum_nats
Proof 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
Proof 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
Theorem: sum_nats
Proof 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]
Proof 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
Theorem: sum_nats
Proof 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]
Proof state after:
no goals
Theorem: sum_nats
Proof 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 [*]
Proof state after:
no goals
Theorem: sum_nats
Proof 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 = _
Proof 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
Theorem: sum_nats
Proof 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]
Proof 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
Theorem: sum_nats
Proof 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
Proof state after:
no goals
Theorem: sum_n
Proof state before:
n j : ℕ
inst✝ : NeZero n
⊢ sum (fun i => i + i / (n + 1) + 1) (j + j / n) = 3 * (j ^ 2 + j) + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: sumDrop_three
Proof state before:
⊢ sumDrop 3 pnats = powers 3
Tactic:
funext i
Proof state after:
case h
i : ℕ
⊢ sumDrop 3 pnats i = powers 3 i
Theorem: sumDrop_three
Proof state before:
case h
i : ℕ
⊢ sumDrop 3 pnats i = powers 3 i
Tactic:
simp only [sumDrop, powers, pow_three, 
  dropEveryNth_eq_fun, pnats, Nat.div_one,
  sum_eq_three_even
]
Proof state after:
case h
i : ℕ
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
Theorem: sumDrop_three
Proof state before:
case h
i : ℕ
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
Tactic:
induction' i with i ih
Proof state after:
case h.zero

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

case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) (Nat.succ i) = (Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))
Theorem: sumDrop_three
Proof state before:
case h.zero

⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) Nat.zero = (Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: sumDrop_three
Proof state before:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ sum (fun i => 3 * (i ^ 2 + i) + 1) (Nat.succ i) = (Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))
Tactic:
simp [ih, show Nat.succ i = i + 1 from rfl]
Proof state after:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ (i + 1) * ((i + 1) * (i + 1)) + (3 * ((i + 1) ^ 2 + (i + 1)) + 1) = (i + 1 + 1) * ((i + 1 + 1) * (i + 1 + 1))
Theorem: sumDrop_three
Proof state before:
case h.succ
i : ℕ
ih : sum (fun i => 3 * (i ^ 2 + i) + 1) i = (i + 1) * ((i + 1) * (i + 1))
⊢ (i + 1) * ((i + 1) * (i + 1)) + (3 * ((i + 1) ^ 2 + (i + 1)) + 1) = (i + 1 + 1) * ((i + 1 + 1) * (i + 1 + 1))
Tactic:
ring
Proof state after:
no goals
Theorem: sumDrop_four
Proof state before:
⊢ sumDrop 4 pnats = powers 4
Tactic:
funext i
Proof state after:
case h
i : ℕ
⊢ sumDrop 4 pnats i = powers 4 i
Theorem: sumDrop_four
Proof state before:
case h
i : ℕ
⊢ sumDrop 4 pnats i = powers 4 i
Tactic:
simp only [sumDrop, powers, pow_succ, pow_zero, mul_one, 
  dropEveryNth_eq_fun, pnats, Nat.div_one
]
Proof state after:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
Theorem: sumDrop_four
Proof state before:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
Tactic:
induction' i with i ih
Proof state after:
case h.zero

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

case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1)))
Theorem: sumDrop_four
Proof state before:
case h.zero

⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1)))
Tactic:
rfl
Proof state after:
no goals
Theorem: sumDrop_four
Proof state before:
case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1)))
Tactic:
sorry
Proof state after:
no goals
Theorem: sumDrop_five
Proof state before:
⊢ sumDrop 5 pnats = powers 5
Tactic:
funext i
Proof state after:
case h
i : ℕ
⊢ sumDrop 5 pnats i = powers 5 i
Theorem: sumDrop_five
Proof state before:
case h
i : ℕ
⊢ sumDrop 5 pnats i = powers 5 i
Tactic:
simp only [sumDrop, powers, pow_succ, pow_zero, mul_one, 
  dropEveryNth_eq_fun, pnats, Nat.div_one
]
Proof state after:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
Theorem: sumDrop_five
Proof state before:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
Tactic:
induction' i with i ih
Proof state after:
case h.zero

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

case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i))
      (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))))
Theorem: sumDrop_five
Proof state before:
case h.zero

⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((Nat.zero + 1) * ((Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1))))
Tactic:
rfl
Proof state after:
no goals
Theorem: sumDrop_five
Proof state before:
case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i))
      (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))))
Tactic:
sorry
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_of_le
Proof state before:
a b : Nat
⊢ a ≤ b → Nat.max a b = b
Tactic:
intro h
Proof state after:
a b : Nat
h : a ≤ b
⊢ Nat.max a b = b
Theorem: Mt.Utils.Nat.max_of_le
Proof state before:
a b : Nat
h : a ≤ b
⊢ Nat.max a b = b
Tactic:
simp only [Nat.max, h, ite_true]
Proof state after:
a b : Nat
h : a ≤ b
⊢ max a b = b
Theorem: Mt.Utils.Nat.max_of_eq'
Proof state before:
a b : Nat
h : a = b
⊢ a ≤ b
Tactic:
rw [h]
Proof state after:
a b : Nat
h : a = b
⊢ b ≤ b
Theorem: Mt.Utils.Nat.max_of_eq'
Proof state before:
a b : Nat
h : a = b
⊢ b ≤ b
Tactic:
constructor
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_of_eq
Proof state before:
a b : Nat
⊢ a = b → Nat.max a b = a
Tactic:
intro h
Proof state after:
a b : Nat
h : a = b
⊢ Nat.max a b = a
Theorem: Mt.Utils.Nat.max_of_eq
Proof state before:
a b : Nat
h : a = b
⊢ Nat.max a b = a
Tactic:
rw [max_of_eq' h]
Proof state after:
a b : Nat
h : a = b
⊢ b = a
Theorem: Mt.Utils.Nat.max_of_eq
Proof state before:
a b : Nat
h : a = b
⊢ b = a
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_of_gt
Proof state before:
a b : Nat
⊢ a > b → Nat.max a b = a
Tactic:
intro h
Proof state after:
a b : Nat
h : a > b
⊢ Nat.max a b = a
Theorem: Mt.Utils.Nat.max_of_gt
Proof state before:
a b : Nat
h : a > b
⊢ Nat.max a b = a
Tactic:
simp only [Nat.max, Nat.not_le_of_gt h, ite_false]
Proof state after:
a b : Nat
h : a > b
⊢ max a b = a
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
a b : Nat
⊢ a ≥ b → Nat.max a b = a
Tactic:
intro h
Proof state after:
a b : Nat
h : a ≥ b
⊢ Nat.max a b = a
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
a b : Nat
h : a ≥ b
⊢ Nat.max a b = a
Tactic:
cases Nat.eq_or_lt_of_le h <;> rename_i h
Proof state after:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a

case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a

case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
. exact max_of_eq h.symm
Proof state after:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
. exact max_of_gt h
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
case inl
a b : Nat
h✝ : a ≥ b
h : b = a
⊢ Nat.max a b = a
Tactic:
exact max_of_eq h.symm
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_of_ge
Proof state before:
case inr
a b : Nat
h✝ : a ≥ b
h : b < a
⊢ Nat.max a b = a
Tactic:
exact max_of_gt h
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
⊢ ∀ (a b : Nat), Nat.max a b = Nat.max b a
Tactic:
intro a b
Proof state after:
a b : Nat
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
a b : Nat
⊢ Nat.max a b = Nat.max b a
Tactic:
cases Nat.lt_or_ge a b <;> rename_i h
Proof state after:
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a

case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a

case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_lt h, max_of_gt h]
Proof state after:
case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr
a b : Nat
h : a ≥ b
⊢ Nat.max a b = Nat.max b a
Tactic:
cases Nat.eq_or_lt_of_le h <;> (clear h ; rename_i h)
Proof state after:
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a

case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a

case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_eq h, max_of_eq' h.symm]
Proof state after:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
. rw [max_of_lt h, max_of_gt h]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inl
a b : Nat
h : a < b
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_lt h, max_of_gt h]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inr
a b : Nat
h : a ≥ b
h✝ : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
clear h
Proof state after:
case inr.inr
a b : Nat
h✝ : b < a
⊢ Nat.max a b = Nat.max b a
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inr
a b : Nat
h✝ : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
rename_i h
Proof state after:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a