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

State before:
m : ℕ
X : ZMod m
⊢ X * [1]_m = X
Tactic:
obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
State after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X * [1]_m = X

State before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X * [1]_m = X
Tactic:
rewrite [h1]
State after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ [a]_m * [1]_m = [a]_m

State before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ [a]_m * [1]_m = [a]_m
Tactic:
have h2 : a * 1 = a := by ring
State after:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a]_m * [1]_m = [a]_m

State before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a]_m * [1]_m = [a]_m
Tactic:
show [a]_m * [1]_m = [a]_m from
  calc [a]_m * [1]_m
    _ = [a * 1]_m := mul_class m a 1
    _ = [a]_m := by rw [h2]
State after:
no goals

State before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ a * 1 = a
Tactic:
ring
State after:
no goals

State before:
m : ℕ
X : ZMod m
a : ℤ
h1 : X = [a]_m
h2 : a * 1 = a
⊢ [a * 1]_m = [a]_m
Tactic:
rw [h2]
State after:
no goals