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

State before:
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m ↔ [a - b]_m = [0]_m
Tactic:
apply Iff.intro
State after:
case mp
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m → [a - b]_m = [0]_m

case mpr
m : ℕ
a b : ℤ
⊢ [a - b]_m = [0]_m → [a]_m = [b]_m

State before:
case mp
m : ℕ
a b : ℤ
⊢ [a]_m = [b]_m → [a - b]_m = [0]_m
Tactic:
assume h1 : [a]_m = [b]_m
State after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
⊢ [a - b]_m = [0]_m

State before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
⊢ [a - b]_m = [0]_m
Tactic:
have h2 : a - b = a + (-b) := by ring
State after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
⊢ [a - b]_m = [0]_m

State before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
⊢ [a - b]_m = [0]_m
Tactic:
have h3 : b + (-b) = 0 := by ring
State after:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a - b]_m = [0]_m

State before:
case mp
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a - b]_m = [0]_m
Tactic:
show [a - b]_m = [0]_m from
  calc [a - b]_m
    _ = [a + (-b)]_m := by rw [h2]
    _ = [a]_m + [-b]_m := by rw [add_class]
    _ = [b]_m + [-b]_m := by rw [h1]
    _ = [b + -b]_m := by rw [add_class]
    _ = [0]_m := by rw [h3]
State after:
no goals

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

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

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

State before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [a + -b]_m = [a]_m + [-b]_m
Tactic:
rw [add_class]
State after:
no goals

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

State before:
m : ℕ
a b : ℤ
h1 : [a]_m = [b]_m
h2 : a - b = a + -b
h3 : b + -b = 0
⊢ [b]_m + [-b]_m = [b + -b]_m
Tactic:
rw [add_class]
State after:
no goals

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

State before:
case mpr
m : ℕ
a b : ℤ
⊢ [a - b]_m = [0]_m → [a]_m = [b]_m
Tactic:
assume h1 : [a - b]_m = [0]_m
State after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ [a]_m = [b]_m

State before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ [a]_m = [b]_m
Tactic:
have h2 : b + (a - b) = a := by ring
State after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ [a]_m = [b]_m

State before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ [a]_m = [b]_m
Tactic:
have h3 : b + 0 = b := by ring
State after:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b]_m

State before:
case mpr
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b]_m
Tactic:
show [a]_m = [b]_m from
  calc [a]_m
    _ = [b + (a - b)]_m := by rw [h2]
    _ = [b]_m + [a - b]_m := by rw [add_class]
    _ = [b]_m + [0]_m := by rw [h1]
    _ = [b + 0]_m := by rw [add_class]
    _ = [b]_m := by rw [h3]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
⊢ b + (a - b) = a
Tactic:
ring
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
⊢ b + 0 = b
Tactic:
ring
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [a]_m = [b + (a - b)]_m
Tactic:
rw [h2]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b + (a - b)]_m = [b]_m + [a - b]_m
Tactic:
rw [add_class]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b]_m + [a - b]_m = [b]_m + [0]_m
Tactic:
rw [h1]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b]_m + [0]_m = [b + 0]_m
Tactic:
rw [add_class]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : [a - b]_m = [0]_m
h2 : b + (a - b) = a
h3 : b + 0 = b
⊢ [b + 0]_m = [b]_m
Tactic:
rw [h3]
State after:
no goals