Theorem: Poland1998P4.can_get_a_later_one_zmod (Compfiles/Poland1998P4.lean)

State before:
⊢ ∀ (N : ℕ), a' N = 0 → ∃ M, N < M ∧ a' M = 0
Tactic:
intro n hn
State after:
n : ℕ
hn : a' n = 0
⊢ ∃ M, n < M ∧ a' M = 0

State before:
n : ℕ
hn : a' n = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
obtain (hlt : n < 2) | (hlte : 2 ≤ n) := lt_or_ge n 2
State after:
case inl
n : ℕ
hn : a' n = 0
hlt : n < 2
⊢ ∃ M, n < M ∧ a' M = 0

case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
⊢ ∃ M, n < M ∧ a' M = 0

State before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
let n1 : ℕ := 2 * (n - 1) + 1
State after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ ∃ M, n < M ∧ a' M = 0

State before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have npos := calc 0 < 2 := by norm_num
                  _ ≤ n := hlte
State after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
⊢ ∃ M, n < M ∧ a' M = 0

State before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have hn1v : n1 = 2 * n - 1 := lemma1 n npos
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
⊢ ∃ M, n < M ∧ a' M = 0

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
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have hn2 : 2 ≤ n1 + 1 := Nat.succ_le_succ le_add_self
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
⊢ ∃ M, n < M ∧ a' M = 0

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
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
let an1 := a' n1
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
⊢ ∃ M, n < M ∧ a' M = 0

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
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha1 : a' (n1 + 1) = an1 + a' n := by
  have haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2) := a'_recurrence (n1 + 1) hn2
  have h2n1 : 2 * n / 2 = n := by norm_num
  have h2n1' : (n1 + 1) / 2 = n := by rw [hn1, h2n1]
  rw [haa, h2n1']
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
⊢ ∃ M, n < M ∧ a' M = 0

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
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha2 : a' (n1 + 2) = a' (n1 + 1) +  a' n := by
  have haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2) :=
    a'_recurrence (n1 + 2) le_add_self
  have h1 : (2 * n + 1) / 2 = n := lemma2 n
  have hn1v' : 2 * n = n1 + 1 := hn1.symm
  rw [haa]
  congr
  have : n1.succ.succ = (n1 + 1 + 1) := rfl
  rw [this, ←hn1v', h1]
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
⊢ ∃ M, n < M ∧ a' M = 0

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
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha1' : a' (n1 + 1) = a' n1 := by
  simp only [hn, add_zero] at ha1
  exact ha1
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
⊢ ∃ M, n < M ∧ a' M = 0

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
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

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
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

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
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

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)
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

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]⟩
State after:
no goals

State before:
n : ℕ
hn : a' n = 0
hlt : n < 2
⊢ a' 5 = 0
Tactic:
simp [a', a]
State after:
no goals

State before:
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

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
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

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]
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

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
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)

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
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

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']
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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

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
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

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
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

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]
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

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
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

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
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

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]
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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)

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
State after:
no goals

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
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)

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
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)

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
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)

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
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)

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
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)

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
hi6 : p < 7
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hpp := hp hi6
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
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)

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
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hp1: (p.succ : ZMod 7) = (p : ZMod 7) + 1 := Nat.cast_succ p
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
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)

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
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
rw [←hadd, hinc, hpp, hp1]
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
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' n2 + a' n1 * ↑p + a' n1 = a' n2 + a' n1 * (↑p + 1)

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
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' n2 + a' n1 * ↑p + a' n1 = a' n2 + a' n1 * (↑p + 1)
Tactic:
ring
State after:
no goals

State before:
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
Tactic:
use n1
State after:
case h
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
⊢ n < n1 ∧ a' n1 = 0

State before:
case h
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
⊢ n < n1 ∧ a' n1 = 0
Tactic:
constructor
State after:
case h.left
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
⊢ n < n1

case h.right
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
⊢ a' n1 = 0

State before:
case h.left
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
⊢ n < n1
Tactic:
omega
State after:
no goals

State before:
case h.right
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
⊢ a' n1 = 0
Tactic:
exact haez
State after:
no goals

State before:
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
Tactic:
have := lemma3 n2 (a' n1) hanez hik
State after:
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
this : ∃ i < 7, a' (n2 + i) = 0
⊢ ∃ M, n < M ∧ a' M = 0

State before:
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
this : ∃ i < 7, a' (n2 + i) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
obtain ⟨ii, _, hia'⟩ := this
State after:
case inr.inr.intro.intro
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ ∃ M, n < M ∧ a' M = 0

State before:
case inr.inr.intro.intro
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
use (n2 + ii)
State after:
case h
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii ∧ a' (n2 + ii) = 0

State before:
case h
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii ∧ a' (n2 + ii) = 0
Tactic:
constructor
State after:
case h.left
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii

case h.right
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ a' (n2 + ii) = 0

State before:
case h.left
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii
Tactic:
linarith
State after:
no goals

State before:
case h.right
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
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ a' (n2 + ii) = 0
Tactic:
assumption
State after:
no goals