Theorem: Usa2003P1.nat_mod_inv (Compfiles/Usa2003P1.lean)

State before:
a : ℕ
⊢ ∃ b, (a + b) % 5 = 0
Tactic:
use 5 - (a % 5)
State after:
case h
a : ℕ
⊢ (a + (5 - a % 5)) % 5 = 0

State before:
case h
a : ℕ
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
have h : a % 5 < 5 := Nat.mod_lt _ (by norm_num)
State after:
case h
a : ℕ
h : a % 5 < 5
⊢ (a + (5 - a % 5)) % 5 = 0

State before:
case h
a : ℕ
h : a % 5 < 5
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
have h' : a % 5 ≤ 5 := Nat.le_of_lt h
State after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a + (5 - a % 5)) % 5 = 0

State before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a + (5 - a % 5)) % 5 = 0
Tactic:
rw[Nat.add_mod]
State after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0

State before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Tactic:
have h2 : a % 5 = a % 5 % 5 := (Nat.mod_mod a 5).symm
State after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0

State before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5) % 5) % 5 = 0
Tactic:
rw[h2, ← Nat.add_mod, Nat.mod_mod]
State after:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5)) % 5 = 0

State before:
case h
a : ℕ
h : a % 5 < 5
h' : a % 5 ≤ 5
h2 : a % 5 = a % 5 % 5
⊢ (a % 5 + (5 - a % 5)) % 5 = 0
Tactic:
rw[Nat.add_sub_of_le h']
State after:
no goals

State before:
a : ℕ
⊢ 5 > 0
Tactic:
norm_num
State after:
no goals