Theorem: Poland1998P4.poland1998_p4' (Compfiles/Poland1998P4.lean)

State before:
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M
Tactic:
have he : 7 ∣ a 5 := by simp [a', a]
State after:
he : 7 ∣ a 5
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M

State before:
he : 7 ∣ a 5
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M
Tactic:
exact strengthen can_get_a_later_one ⟨5, he⟩
State after:
no goals

State before:
⊢ 7 ∣ a 5
Tactic:
simp [a', a]
State after:
no goals