Theorem: Imo1994P1.tedious (Compfiles/Imo1994P1.lean)

State before:
m : ℕ
k : Fin (m + 1)
⊢ m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k
Tactic:
cases' k with k hk
State after:
case mk
m k : ℕ
hk : k < m + 1
⊢ m - (m + (m + 1 - ↑⟨k, hk⟩)) % (m + 1) = ↑⟨k, hk⟩

State before:
case mk
m k : ℕ
hk : k < m + 1
⊢ m - (m + (m + 1 - ↑⟨k, hk⟩)) % (m + 1) = ↑⟨k, hk⟩
Tactic:
rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
State after:
case mk
m k : ℕ
hk✝ : k < m + 1
hk : ∃ c, m = k + c
⊢ m - (m + (m + 1 - ↑⟨k, hk✝⟩)) % (m + 1) = ↑⟨k, hk✝⟩

State before:
case mk
m k : ℕ
hk✝ : k < m + 1
hk : ∃ c, m = k + c
⊢ m - (m + (m + 1 - ↑⟨k, hk✝⟩)) % (m + 1) = ↑⟨k, hk✝⟩
Tactic:
rcases hk with ⟨c, rfl⟩
State after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩

State before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Tactic:
have : k + c + (k + c + 1 - k) = c + (k + c + 1) := by
  simp only [add_assoc, add_tsub_cancel_left, add_left_comm]
State after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩

State before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Tactic:
rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
State after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ c < k + c + 1

State before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ c < k + c + 1
Tactic:
omega
State after:
no goals

State before:
k c : ℕ
hk : k < k + c + 1
⊢ k + c + (k + c + 1 - k) = c + (k + c + 1)
Tactic:
simp only [add_assoc, add_tsub_cancel_left, add_left_comm]
State after:
no goals