internlm/Lean-Github huggingface dataset:
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1' : a' (n1 + 1) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha2' : a' (n1 + 2) = a' n1 := by
  rw [hn, ha1'] at ha2
  simp at ha2
  exact ha2
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
clear ha1 ha2
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
let n2 : ℕ := 4 * (n - 1) + 1
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
obtain (haez : a' n1 = 0) | (hanez : ¬ a' n1 = 0) := em (a' n1 = 0)
Proof state after:
case inr.inl
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ ∃ M, n < M ∧ a' M = 0

case inr.inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inl
n : ℕ
hn : a' n = 0
hlt : n < 2
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
exact ⟨5, Nat.le.step <| Nat.le.step <| Nat.le.step hlt, by simp [a', a]⟩
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlt : n < 2
⊢ a' 5 = 0
Tactic:
simp [a', a]
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
⊢ n1 + 1 = 2 * n
Tactic:
have hrw : (n1 + 1) = 2 * (n - 1) + 1 + 1 := rfl
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n - 1) + 1 + 1
⊢ n1 + 1 = 2 * n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n - 1) + 1 + 1
⊢ n1 + 1 = 2 * n
Tactic:
rw [hrw]
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n - 1) + 1 + 1
⊢ 2 * (n - 1) + 1 + 1 = 2 * n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n - 1) + 1 + 1
⊢ 2 * (n - 1) + 1 + 1 = 2 * n
Tactic:
cases' n
Proof state after:
case zero
hn : a' 0 = 0
hlte : 2 ≤ 0
n1 : ℕ := 2 * (0 - 1) + 1
npos : 0 < 0
hn1v : n1 = 2 * 0 - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (0 - 1) + 1 + 1
⊢ 2 * (0 - 1) + 1 + 1 = 2 * 0

case succ
n✝ : ℕ
hn : a' (n✝ + 1) = 0
hlte : 2 ≤ n✝ + 1
n1 : ℕ := 2 * (n✝ + 1 - 1) + 1
npos : 0 < n✝ + 1
hn1v : n1 = 2 * (n✝ + 1) - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n✝ + 1 - 1) + 1 + 1
⊢ 2 * (n✝ + 1 - 1) + 1 + 1 = 2 * (n✝ + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case zero
hn : a' 0 = 0
hlte : 2 ≤ 0
n1 : ℕ := 2 * (0 - 1) + 1
npos : 0 < 0
hn1v : n1 = 2 * 0 - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (0 - 1) + 1 + 1
⊢ 2 * (0 - 1) + 1 + 1 = 2 * 0
Tactic:
exfalso
Proof state after:
case zero
hn : a' 0 = 0
hlte : 2 ≤ 0
n1 : ℕ := 2 * (0 - 1) + 1
npos : 0 < 0
hn1v : n1 = 2 * 0 - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (0 - 1) + 1 + 1
⊢ False
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case zero
hn : a' 0 = 0
hlte : 2 ≤ 0
n1 : ℕ := 2 * (0 - 1) + 1
npos : 0 < 0
hn1v : n1 = 2 * 0 - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (0 - 1) + 1 + 1
⊢ False
Tactic:
exact lt_asymm npos npos
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
n✝ : ℕ
hn : a' (n✝ + 1) = 0
hlte : 2 ≤ n✝ + 1
n1 : ℕ := 2 * (n✝ + 1 - 1) + 1
npos : 0 < n✝ + 1
hn1v : n1 = 2 * (n✝ + 1) - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n✝ + 1 - 1) + 1 + 1
⊢ 2 * (n✝ + 1 - 1) + 1 + 1 = 2 * (n✝ + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
⊢ a' (n1 + 1) = an1 + a' n
Tactic:
have haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2) := a'_recurrence (n1 + 1) hn2
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
⊢ a' (n1 + 1) = an1 + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
⊢ a' (n1 + 1) = an1 + a' n
Tactic:
have h2n1 : 2 * n / 2 = n := by norm_num
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
h2n1 : 2 * n / 2 = n
⊢ a' (n1 + 1) = an1 + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
h2n1 : 2 * n / 2 = n
⊢ a' (n1 + 1) = an1 + a' n
Tactic:
have h2n1' : (n1 + 1) / 2 = n := by rw [hn1, h2n1]
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
h2n1 : 2 * n / 2 = n
h2n1' : (n1 + 1) / 2 = n
⊢ a' (n1 + 1) = an1 + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
h2n1 : 2 * n / 2 = n
h2n1' : (n1 + 1) / 2 = n
⊢ a' (n1 + 1) = an1 + a' n
Tactic:
rw [haa, h2n1']
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
⊢ 2 * n / 2 = n
Tactic:
norm_num
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2)
h2n1 : 2 * n / 2 = n
⊢ (n1 + 1) / 2 = n
Tactic:
rw [hn1, h2n1]
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Tactic:
have haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2) :=
  a'_recurrence (n1 + 2) le_add_self
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Tactic:
have h1 : (2 * n + 1) / 2 = n := lemma2 n
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Tactic:
have hn1v' : 2 * n = n1 + 1 := hn1.symm
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ a' (n1 + 2) = a' (n1 + 1) + a' n
Tactic:
rw [haa]
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ a' (n1 + 1) + a' (n1.succ.succ / 2) = a' (n1 + 1) + a' n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ a' (n1 + 1) + a' (n1.succ.succ / 2) = a' (n1 + 1) + a' n
Tactic:
congr
Proof state after:
case e_a.e_a
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ n1.succ.succ / 2 = n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case e_a.e_a
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
⊢ n1.succ.succ / 2 = n
Tactic:
have : n1.succ.succ = (n1 + 1 + 1) := rfl
Proof state after:
case e_a.e_a
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
this : n1.succ.succ = n1 + 1 + 1
⊢ n1.succ.succ / 2 = n
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case e_a.e_a
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2)
h1 : (2 * n + 1) / 2 = n
hn1v' : 2 * n = n1 + 1
this : n1.succ.succ = n1 + 1 + 1
⊢ n1.succ.succ / 2 = n
Tactic:
rw [this, ←hn1v', h1]
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
⊢ a' (n1 + 1) = a' n1
Tactic:
simp only [hn, add_zero] at ha1
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1 : a' (n1 + 1) = an1
⊢ a' (n1 + 1) = a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1 : a' (n1 + 1) = an1
⊢ a' (n1 + 1) = a' n1
Tactic:
exact ha1
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1' : a' (n1 + 1) = a' n1
⊢ a' (n1 + 2) = a' n1
Tactic:
rw [hn, ha1'] at ha2
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' n1 + 0
ha1' : a' (n1 + 1) = a' n1
⊢ a' (n1 + 2) = a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' n1 + 0
ha1' : a' (n1 + 1) = a' n1
⊢ a' (n1 + 2) = a' n1
Tactic:
simp at ha2
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha1' : a' (n1 + 1) = a' n1
ha2 : a' (n1 + 2) = a' n1
⊢ a' (n1 + 2) = a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha1' : a' (n1 + 1) = a' n1
ha2 : a' (n1 + 2) = a' n1
⊢ a' (n1 + 2) = a' n1
Tactic:
exact ha2
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
⊢ ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
Tactic:
intro i hi
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Tactic:
have hn2ge2 : 2 ≤ n2 + i + 1 := by omega
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
hn2ge2 : 2 ≤ n2 + i + 1
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
hn2ge2 : 2 ≤ n2 + i + 1
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Tactic:
have hr := a'_recurrence (n2 + i + 1) hn2ge2
Proof state after:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
hn2ge2 : 2 ≤ n2 + i + 1
hr : a' (n2 + i + 1) = a' (n2 + i + 1 - 1) + a' ((n2 + i + 1) / 2)
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
hn2ge2 : 2 ≤ n2 + i + 1
hr : a' (n2 + i + 1) = a' (n2 + i + 1 - 1) + a' ((n2 + i + 1) / 2)
⊢ a' (n2 + i + 1) = a' (n2 + i) + a' n1
Tactic:
interval_cases i
Proof state after:
case «0»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 0 < 6
hn2ge2 : 2 ≤ n2 + 0 + 1
hr : a' (n2 + 0 + 1) = a' (n2 + 0 + 1 - 1) + a' ((n2 + 0 + 1) / 2)
⊢ a' (n2 + 0 + 1) = a' (n2 + 0) + a' n1

case «1»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 1 < 6
hn2ge2 : 2 ≤ n2 + 1 + 1
hr : a' (n2 + 1 + 1) = a' (n2 + 1 + 1 - 1) + a' ((n2 + 1 + 1) / 2)
⊢ a' (n2 + 1 + 1) = a' (n2 + 1) + a' n1

case «2»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 2 < 6
hn2ge2 : 2 ≤ n2 + 2 + 1
hr : a' (n2 + 2 + 1) = a' (n2 + 2 + 1 - 1) + a' ((n2 + 2 + 1) / 2)
⊢ a' (n2 + 2 + 1) = a' (n2 + 2) + a' n1

case «3»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 3 < 6
hn2ge2 : 2 ≤ n2 + 3 + 1
hr : a' (n2 + 3 + 1) = a' (n2 + 3 + 1 - 1) + a' ((n2 + 3 + 1) / 2)
⊢ a' (n2 + 3 + 1) = a' (n2 + 3) + a' n1

case «4»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 4 < 6
hn2ge2 : 2 ≤ n2 + 4 + 1
hr : a' (n2 + 4 + 1) = a' (n2 + 4 + 1 - 1) + a' ((n2 + 4 + 1) / 2)
⊢ a' (n2 + 4 + 1) = a' (n2 + 4) + a' n1

case «5»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 5 < 6
hn2ge2 : 2 ≤ n2 + 5 + 1
hr : a' (n2 + 5 + 1) = a' (n2 + 5 + 1 - 1) + a' ((n2 + 5 + 1) / 2)
⊢ a' (n2 + 5 + 1) = a' (n2 + 5) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : i < 6
⊢ 2 ≤ n2 + i + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case «0»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 0 < 6
hn2ge2 : 2 ≤ n2 + 0 + 1
hr : a' (n2 + 0 + 1) = a' (n2 + 0 + 1 - 1) + a' ((n2 + 0 + 1) / 2)
⊢ a' (n2 + 0 + 1) = a' (n2 + 0) + a' n1
Tactic:
suffices (n2 + 1) / 2 = n1 by rwa [this] at hr
Proof state after:
case «0»
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1' : a' (n1 + 1) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
i : ℕ
hi : 0 < 6
hn2ge2 : 2 ≤ n2 + 0 + 1
hr : a' (n2 + 0 + 1) = a' (n2 + 0 + 1 - 1) + a' ((n2 + 0 + 1) / 2)
⊢ (n2 + 1) / 2 = n1