internlm/Lean-Github huggingface dataset:
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)
⊢ (n2 + 1) / 2 = n1
Tactic:
have : (4 * (n - 1) + 1 + 1) = 2 * (2 * (n - 1) + 1) := by ring
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)
this : 4 * (n - 1) + 1 + 1 = 2 * (2 * (n - 1) + 1)
⊢ (n2 + 1) / 2 = n1
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)
this : 4 * (n - 1) + 1 + 1 = 2 * (2 * (n - 1) + 1)
⊢ (n2 + 1) / 2 = n1
Tactic:
simp only [this, Nat.succ_pos', Nat.mul_div_right]
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 : ℕ
hi : 0 < 6
hn2ge2 : 2 ≤ n2 + 0 + 1
hr : a' (n2 + 0 + 1) = a' (n2 + 0 + 1 - 1) + a' ((n2 + 0 + 1) / 2)
this : (n2 + 1) / 2 = n1
⊢ a' (n2 + 0 + 1) = a' (n2 + 0) + a' n1
Tactic:
rwa [this] at hr
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 : ℕ
hi : 0 < 6
hn2ge2 : 2 ≤ n2 + 0 + 1
hr : a' (n2 + 0 + 1) = a' (n2 + 0 + 1 - 1) + a' ((n2 + 0 + 1) / 2)
⊢ 4 * (n - 1) + 1 + 1 = 2 * (2 * (n - 1) + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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
Tactic:
suffices hn1 : (n2 + 2) / 2 = n1 by rwa [hn1] at hr
Proof state after:
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)
⊢ (n2 + 2) / 2 = n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
⊢ (n2 + 2) / 2 = n1
Tactic:
have h1 : (4 * (n - 1) + 1 + 2) = 2 * (2 * (n - 1) + 1) + 1 := by ring
Proof state after:
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)
h1 : 4 * (n - 1) + 1 + 2 = 2 * (2 * (n - 1) + 1) + 1
⊢ (n2 + 2) / 2 = n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
h1 : 4 * (n - 1) + 1 + 2 = 2 * (2 * (n - 1) + 1) + 1
⊢ (n2 + 2) / 2 = n1
Tactic:
rw [h1]
Proof state after:
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)
h1 : 4 * (n - 1) + 1 + 2 = 2 * (2 * (n - 1) + 1) + 1
⊢ (2 * (2 * (n - 1) + 1) + 1) / 2 = n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
h1 : 4 * (n - 1) + 1 + 2 = 2 * (2 * (n - 1) + 1) + 1
⊢ (2 * (2 * (n - 1) + 1) + 1) / 2 = n1
Tactic:
exact lemma2 (2 * (n - 1) + 1)
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 : ℕ
hi : 1 < 6
hn2ge2 : 2 ≤ n2 + 1 + 1
hr : a' (n2 + 1 + 1) = a' (n2 + 1 + 1 - 1) + a' ((n2 + 1 + 1) / 2)
hn1 : (n2 + 2) / 2 = n1
⊢ a' (n2 + 1 + 1) = a' (n2 + 1) + a' n1
Tactic:
rwa [hn1] at hr
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 : ℕ
hi : 1 < 6
hn2ge2 : 2 ≤ n2 + 1 + 1
hr : a' (n2 + 1 + 1) = a' (n2 + 1 + 1 - 1) + a' ((n2 + 1 + 1) / 2)
⊢ 4 * (n - 1) + 1 + 2 = 2 * (2 * (n - 1) + 1) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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
Tactic:
have hn1 : (n2 + 3) / 2 = n1 + 1 := lemma6 n
Proof state after:
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)
hn1 : (n2 + 3) / 2 = n1 + 1
⊢ a' (n2 + 2 + 1) = a' (n2 + 2) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
hn1 : (n2 + 3) / 2 = n1 + 1
⊢ a' (n2 + 2 + 1) = a' (n2 + 2) + a' n1
Tactic:
rw [hn1, ha1'] at hr
Proof state after:
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' n1
hn1 : (n2 + 3) / 2 = n1 + 1
⊢ a' (n2 + 2 + 1) = a' (n2 + 2) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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' n1
hn1 : (n2 + 3) / 2 = n1 + 1
⊢ a' (n2 + 2 + 1) = a' (n2 + 2) + a' n1
Tactic:
exact hr
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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
Tactic:
have hn1 : (n2 + 4) / 2 = n1 + 1 := lemma6' n
Proof state after:
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)
hn1 : (n2 + 4) / 2 = n1 + 1
⊢ a' (n2 + 3 + 1) = a' (n2 + 3) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
hn1 : (n2 + 4) / 2 = n1 + 1
⊢ a' (n2 + 3 + 1) = a' (n2 + 3) + a' n1
Tactic:
rw [hn1, ha1'] at hr
Proof state after:
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' n1
hn1 : (n2 + 4) / 2 = n1 + 1
⊢ a' (n2 + 3 + 1) = a' (n2 + 3) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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' n1
hn1 : (n2 + 4) / 2 = n1 + 1
⊢ a' (n2 + 3 + 1) = a' (n2 + 3) + a' n1
Tactic:
exact hr
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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
Tactic:
have hn1 : (n2 + 5) / 2 = n1 + 2 := lemma7 n
Proof state after:
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)
hn1 : (n2 + 5) / 2 = n1 + 2
⊢ a' (n2 + 4 + 1) = a' (n2 + 4) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
hn1 : (n2 + 5) / 2 = n1 + 2
⊢ a' (n2 + 4 + 1) = a' (n2 + 4) + a' n1
Tactic:
rw [hn1, ha2'] at hr
Proof state after:
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' n1
hn1 : (n2 + 5) / 2 = n1 + 2
⊢ a' (n2 + 4 + 1) = a' (n2 + 4) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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' n1
hn1 : (n2 + 5) / 2 = n1 + 2
⊢ a' (n2 + 4 + 1) = a' (n2 + 4) + a' n1
Tactic:
exact hr
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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
Tactic:
have hn1 : (n2 + 6) / 2 = n1 + 2 := lemma7' n
Proof state after:
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)
hn1 : (n2 + 6) / 2 = n1 + 2
⊢ a' (n2 + 5 + 1) = a' (n2 + 5) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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)
hn1 : (n2 + 6) / 2 = n1 + 2
⊢ a' (n2 + 5 + 1) = a' (n2 + 5) + a' n1
Tactic:
rw [hn1, ha2'] at hr
Proof state after:
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' n1
hn1 : (n2 + 6) / 2 = n1 + 2
⊢ a' (n2 + 5 + 1) = a' (n2 + 5) + a' n1
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
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' n1
hn1 : (n2 + 6) / 2 = n1 + 2
⊢ a' (n2 + 5 + 1) = a' (n2 + 5) + a' n1
Tactic:
exact hr
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
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
⊢ ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
Tactic:
intro i
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
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
i : ℕ
⊢ i < 7 → a' (n2 + i) = a' n2 + a' n1 * ↑i
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
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
i : ℕ
⊢ i < 7 → a' (n2 + i) = a' n2 + a' n1 * ↑i
Tactic:
induction' i with p hp
Proof state after:
case zero
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
⊢ 0 < 7 → a' (n2 + 0) = a' n2 + a' n1 * ↑0

case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ p + 1 < 7 → a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case zero
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
⊢ 0 < 7 → a' (n2 + 0) = a' n2 + a' n1 * ↑0
Tactic:
simp
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ p + 1 < 7 → a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
intro hpi7
Proof state after:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hpi6 : p < 6 := Nat.succ_lt_succ_iff.mp hpi7
Proof state after:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hinc := hii p hpi6
Proof state after:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hadd : n2 + p + 1 = n2 + p.succ := rfl
Proof state after:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hi6 : p < 7 := Nat.lt.step hpi6
Proof state after:
case succ
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
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)