Theorem: Poland1998P4.zmod_ext (Compfiles/Poland1998P4.lean)

State before:
a b : ZMod 7
hz : a.val = b.val
⊢ a = b
Tactic:
have : ((ZMod.val a) : ZMod 7)  = ((ZMod.val b) : ZMod 7) := congrArg Nat.cast hz
State after:
a b : ZMod 7
hz : a.val = b.val
this : ↑a.val = ↑b.val
⊢ a = b

State before:
a b : ZMod 7
hz : a.val = b.val
this : ↑a.val = ↑b.val
⊢ a = b
Tactic:
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq] at this
State after:
a b : ZMod 7
hz : a.val = b.val
this : a = b
⊢ a = b

State before:
a b : ZMod 7
hz : a.val = b.val
this : a = b
⊢ a = b
Tactic:
exact this
State after:
no goals