Theorem: HTPI.congr_refl (HTPILib/Chap7.lean)

State before:
m : ℕ
⊢ ∀ (a : ℤ), a ≡ a (MOD m)
Tactic:
fix a : Int
State after:
m : ℕ
a : ℤ
⊢ a ≡ a (MOD m)

State before:
m : ℕ
a : ℤ
⊢ a ≡ a (MOD m)
Tactic:
define
State after:
m : ℕ
a : ℤ
⊢ ∃ c, a - a = ↑m * c

State before:
m : ℕ
a : ℤ
⊢ ∃ c, a - a = ↑m * c
Tactic:
apply Exists.intro 0
State after:
m : ℕ
a : ℤ
⊢ a - a = ↑m * 0

State before:
m : ℕ
a : ℤ
⊢ a - a = ↑m * 0
Tactic:
ring
State after:
no goals