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

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

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
⊢ X + Y = Y + X
Tactic:
obtain (b : Int) (h2 : Y = [b]_m) from cc_rep Y
State after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ X + Y = Y + X

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ X + Y = Y + X
Tactic:
rewrite [h1, h2]
State after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ [a]_m + [b]_m = [b]_m + [a]_m

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Tactic:
have h3 : a + b = b + a := by ring
State after:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a]_m + [b]_m = [b]_m + [a]_m

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a]_m + [b]_m = [b]_m + [a]_m
Tactic:
show [a]_m + [b]_m = [b]_m + [a]_m from
  calc [a]_m + [b]_m
    _ = [a + b]_m := add_class m a b
    _ = [b + a]_m := by rw [h3]
    _ = [b]_m + [a]_m := (add_class m b a).symm
State after:
no goals

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
⊢ a + b = b + a
Tactic:
ring
State after:
no goals

State before:
m : ℕ
X Y : ZMod m
a : ℤ
h1 : X = [a]_m
b : ℤ
h2 : Y = [b]_m
h3 : a + b = b + a
⊢ [a + b]_m = [b + a]_m
Tactic:
rw [h3]
State after:
no goals