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

State before:
⊢ ∀ (N : ℕ), 7 ∣ a N → ∃ M, N < M ∧ 7 ∣ Poland1998P4.a M
Tactic:
intro n hn
State after:
n : ℕ
hn : 7 ∣ a n
⊢ ∃ M, n < M ∧ 7 ∣ a M

State before:
n : ℕ
hn : 7 ∣ a n
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
have ha' : a' n = 0 := by
  have : a' n = ⟨a n % 7, Nat.mod_lt _ (Nat.succ_pos _)⟩ := by simp[a']
  rw [this]
  simp only [Nat.mod_eq_zero_of_dvd hn, Fin.mk_zero]
State after:
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M

State before:
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
obtain ⟨m, hmgt, hm7⟩ := can_get_a_later_one_zmod n ha'
State after:
case intro.intro
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M

State before:
case intro.intro
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
use m
State after:
case h
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ n < m ∧ 7 ∣ a m

State before:
case h
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ n < m ∧ 7 ∣ a m
Tactic:
use hmgt
State after:
case right
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ 7 ∣ a m

State before:
case right
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ 7 ∣ a m
Tactic:
exact Fin.natCast_eq_zero.mp hm7
State after:
no goals

State before:
n : ℕ
hn : 7 ∣ a n
⊢ a' n = 0
Tactic:
have : a' n = ⟨a n % 7, Nat.mod_lt _ (Nat.succ_pos _)⟩ := by simp[a']
State after:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ a' n = 0

State before:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ a' n = 0
Tactic:
rw [this]
State after:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ ⟨a n % 7, ⋯⟩ = 0

State before:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ ⟨a n % 7, ⋯⟩ = 0
Tactic:
simp only [Nat.mod_eq_zero_of_dvd hn, Fin.mk_zero]
State after:
no goals

State before:
n : ℕ
hn : 7 ∣ a n
⊢ a' n = ⟨a n % 7, ⋯⟩
Tactic:
simp[a']
State after:
no goals