Theorem: Poland1998P4.a'_recurrence (Compfiles/Poland1998P4.lean)

State before:
n : ℕ
hn : 2 ≤ n
⊢ a' n = a' (n - 1) + a' (n / 2)
Tactic:
have : (a' n).val = (a' (n - 1) + a' (n / 2)).val := by
  rw [ZMod.val_add]
  simp_rw [a', a_recurrence n hn]
  rw [ZMod.val]
  simp
State after:
n : ℕ
hn : 2 ≤ n
this : (a' n).val = (a' (n - 1) + a' (n / 2)).val
⊢ a' n = a' (n - 1) + a' (n / 2)

State before:
n : ℕ
hn : 2 ≤ n
this : (a' n).val = (a' (n - 1) + a' (n / 2)).val
⊢ a' n = a' (n - 1) + a' (n / 2)
Tactic:
exact zmod_ext _ _ this
State after:
no goals

State before:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = (a' (n - 1) + a' (n / 2)).val
Tactic:
rw [ZMod.val_add]
State after:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = ((a' (n - 1)).val + (a' (n / 2)).val) % 7

State before:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = ((a' (n - 1)).val + (a' (n / 2)).val) % 7
Tactic:
simp_rw [a', a_recurrence n hn]
State after:
n : ℕ
hn : 2 ≤ n
⊢ ZMod.val ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ = (ZMod.val ⟨a (n - 1) % 7, ⋯⟩ + ZMod.val ⟨a (n / 2) % 7, ⋯⟩) % 7

State before:
n : ℕ
hn : 2 ≤ n
⊢ ZMod.val ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ = (ZMod.val ⟨a (n - 1) % 7, ⋯⟩ + ZMod.val ⟨a (n / 2) % 7, ⋯⟩) % 7
Tactic:
rw [ZMod.val]
State after:
n : ℕ
hn : 2 ≤ n
⊢ (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
      | 0 => Int.natAbs
      | n.succ => Fin.val)
      ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ =
    ((match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n - 1) % 7, ⋯⟩ +
        (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n / 2) % 7, ⋯⟩) %
      7

State before:
n : ℕ
hn : 2 ≤ n
⊢ (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
      | 0 => Int.natAbs
      | n.succ => Fin.val)
      ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ =
    ((match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n - 1) % 7, ⋯⟩ +
        (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n / 2) % 7, ⋯⟩) %
      7
Tactic:
simp
State after:
no goals