Theorem: Imo1989P5.lemma4 (Compfiles/Imo1989P5.lean)

State before:
a b : ℕ
h : a ≡ b [MOD b]
⊢ a ≡ 0 [MOD b]
Tactic:
have h1 : a % b = b % b := h
State after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
⊢ a ≡ 0 [MOD b]

State before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
⊢ a ≡ 0 [MOD b]
Tactic:
have h2 : b % b = 0 := Nat.mod_self b
State after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]

State before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = b % b
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Tactic:
rw [h2] at h1
State after:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = 0
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]

State before:
a b : ℕ
h : a ≡ b [MOD b]
h1 : a % b = 0
h2 : b % b = 0
⊢ a ≡ 0 [MOD b]
Tactic:
exact h1
State after:
no goals